consider A being ManySortedSet of I;
take F = id A; :: 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 A) = I by PARTFUN1:def 4;
assume ( i in dom F & F . i = f ) ; :: thesis: f is one-to-one
then f = id (A . i) by A1, Def1;
hence f is one-to-one ; :: thesis: verum