let X be RealNormSpace; :: thesis: for x being sequence of X holds RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))
let x be sequence of X; :: thesis: RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))
set D = RAT_Sums (rng x);
A1: RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x)) by Th17;
the carrier of (NLin (rng x)) c= the carrier of (ClNLin (rng x)) by Th18;
hence RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x)) by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.8866953,"math_prob":0.9861679,"size":499,"snap":"2022-40-2023-06","text_gpt3_token_len":171,"char_repetition_ratio":0.21010101,"word_repetition_ratio":0.38709676,"special_character_ratio":0.31062123,"punctuation_ratio":0.08490566,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99993825,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-10-07T13:18:46Z\",\"WARC-Record-ID\":\"<urn:uuid:920eddc1-801d-44f7-8f39-f0ac56420fe3>\",\"Content-Length\":\"6007\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:6f9a2541-7f42-4991-92d6-f7ac9872d96e>\",\"WARC-Concurrent-To\":\"<urn:uuid:f7a41d5d-962e-46cb-9335-70b61c519ffb>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/normsp_4/22\",\"WARC-Payload-Digest\":\"sha1:6H26GDYCPCRMJEKRBI7AUECGW7YG7MVX\",\"WARC-Block-Digest\":\"sha1:UBZXMVYG27UQ2WHX3ZE2TJIKV6L54NFE\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030338073.68_warc_CC-MAIN-20221007112411-20221007142411-00029.warc.gz\"}"}