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 A1, Def1;
hence f is one-to-one ; :: thesis: verum