let I be set ; :: thesis: for F being ManySortedFunction of I st F is "1-1" holds
for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B

let F be ManySortedFunction of I; :: thesis: ( F is "1-1" implies for A, B being ManySortedSet of I 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 I st A in doms F & B in doms F & F .. A = F .. B holds
A = B

let A, B be ManySortedSet of I; :: 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 :: thesis: for i being object st i in I holds
A . i = B . i
let i be object ; :: thesis: ( i in I implies A . i = B . i )
assume A4: i in I ; :: thesis: A . i = B . i
reconsider f = F . i as Function ;
A5: f is one-to-one by ;
dom f = (doms F) . i by ;
then A6: ( A . i in dom f & B . i in dom f ) by A2, A4;
A7: dom F = I by PARTFUN1:def 2;
then f . (A . i) = (F .. A) . i by
.= f . (B . i) by ;
hence A . i = B . i by A5, A6; :: thesis: verum
end;
hence A = B ; :: thesis: verum