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