let I be set ; :: thesis: for F being ManySortedFunction of st F is "1-1" holds
for A, B being ManySortedSet of st A in doms F & B in doms F & F .. A = F .. B holds
A = B
let F be ManySortedFunction of ; :: thesis: ( F is "1-1" implies for A, B being ManySortedSet of st A in doms F & B in doms F & F .. A = F .. B holds
A = B )
assume A1: F is "1-1" ; :: thesis: for A, B being ManySortedSet of st A in doms F & B in doms F & F .. A = F .. B holds
A = B
let A, B be ManySortedSet of ; :: thesis: ( A in doms F & B in doms F & F .. A = F .. B implies A = B )
assume that
A2: ( A in doms F & B in doms F ) and
A3: F .. A = F .. B ; :: thesis: A = B

now

let i be set ; :: thesis: ( i in I implies A . i = B . i )
assume A4: i in I ; :: thesis: A . i = B . i
A5: dom F = I by PARTFUN1:def 4;
reconsider f = F . i as Function ;
A6: f is one-to-one by A1, A4, MSUALG_3:1;
dom f = (doms F) . i by A4, MSSUBFAM:14;
then A7: ( A . i in dom f & B . i in dom f ) by A2, A4, PBOOLE:def 4;
f . (A . i) = (F .. A) . i by A4, A5, PRALG_1:def 17
.= f . (B . i) by A3, A4, A5, PRALG_1:def 17 ;
hence A . i = B . i by A6, A7, FUNCT_1:def 8; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum