set A = the ManySortedSet of I;
take F = id the ManySortedSet of I; :: thesis: F is "1-1"
let i be set ; :: according to MSUALG_3:def 2 :: thesis: for f being Function st i in dom F & F . i = f holds
f is one-to-one

let f be Function; :: thesis: ( i in dom F & F . i = f implies f is one-to-one )
A1: dom (id the ManySortedSet of I) = I by PARTFUN1:def 2;
assume ( i in dom F & F . i = f ) ; :: thesis: f is one-to-one
then f = id ( the ManySortedSet of I . i) by ;
hence f is one-to-one ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.73947054,"math_prob":0.9888743,"size":443,"snap":"2022-40-2023-06","text_gpt3_token_len":166,"char_repetition_ratio":0.1548975,"word_repetition_ratio":0.18348624,"special_character_ratio":0.37697518,"punctuation_ratio":0.13559322,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9955176,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-10-01T20:39:56Z\",\"WARC-Record-ID\":\"<urn:uuid:a5a5888a-8432-4b03-ad1d-42678dec0141>\",\"Content-Length\":\"5842\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:cc397806-7fd5-4d86-8262-0074087b010b>\",\"WARC-Concurrent-To\":\"<urn:uuid:26901a3f-022f-4034-beb9-fb11dffddb3d>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/msualg_3/5_1_1\",\"WARC-Payload-Digest\":\"sha1:NTSZOUVLHRBXWJXAYXQFA2W5MFYRHE64\",\"WARC-Block-Digest\":\"sha1:MGBTML7MPEMU2DPGX7ZLHVWEBTVZ3UYO\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030336921.76_warc_CC-MAIN-20221001195125-20221001225125-00047.warc.gz\"}"}