let X be set ; :: thesis: for fs being FinSequence of X
for fss being Subset of fs
for m being Element of NAT st m in dom (Seq fss) holds
ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fs be FinSequence of X; :: thesis: for fss being Subset of fs
for m being Element of NAT st m in dom (Seq fss) holds
ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fss be Subset of fs; :: thesis: for m being Element of NAT st m in dom (Seq fss) holds
ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let m be Element of NAT ; :: thesis: ( m in dom (Seq fss) implies ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n ) )

set f = Sgm (dom fss);
set n = (Sgm (dom fss)) . m;
consider k being Nat such that
A1: dom fss c= Seg k by FINSEQ_1:def 12;
assume A2: m in dom (Seq fss) ; :: thesis: ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

then A3: m in dom (fss * (Sgm (dom fss))) by FINSEQ_1:def 14;
then A4: (Sgm (dom fss)) . m in dom fss by FUNCT_1:11;
Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;
then (Seq fss) . m = fss . ((Sgm (dom fss)) . m) by ;
then A5: [((Sgm (dom fss)) . m),((Seq fss) . m)] in fss by ;
then A6: (Sgm (dom fss)) . m in dom fs by FUNCT_1:1;
A7: m in dom (Sgm (dom fss)) by ;
A8: (Seq fss) . m = fs . ((Sgm (dom fss)) . m) by ;
k in NAT by ORDINAL1:def 12;
hence ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n ) by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.697873,"math_prob":0.9995797,"size":1558,"snap":"2019-43-2019-47","text_gpt3_token_len":620,"char_repetition_ratio":0.2084942,"word_repetition_ratio":0.5125628,"special_character_ratio":0.4216945,"punctuation_ratio":0.16747573,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9998005,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-20T17:10:36Z\",\"WARC-Record-ID\":\"<urn:uuid:ba233249-9210-47ef-acd2-2983c3d47487>\",\"Content-Length\":\"21128\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:6f7a73eb-9252-48c0-a7ac-2e89ee42c9e4>\",\"WARC-Concurrent-To\":\"<urn:uuid:99499290-7379-44f2-976d-b3b9175d392f>\",\"WARC-IP-Address\":\"212.33.73.131\",\"WARC-Target-URI\":\"http://mizar.uwb.edu.pl/version/current/html/proofs/glib_001/4\",\"WARC-Payload-Digest\":\"sha1:35V4765KKN6AGW5VTTCLFATVIUT3R3ZP\",\"WARC-Block-Digest\":\"sha1:PM2KQLORNI6VHEOCLPK77SZWZJBSNOWO\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570986717235.56_warc_CC-MAIN-20191020160500-20191020184000-00395.warc.gz\"}"}