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 A1, A4, MSUALG_3:1;
dom f = (doms F) . i by A4, MSSUBFAM:14;
then A6: ( A . i in dom f & B . i in dom f ) by A2, A4;
f . (A . i) = (F .. A) . i by A4, PRALG_1:def 20
.= f . (B . i) by A3, A4, PRALG_1:def 20 ;
hence A . i = B . i by A5, A6; :: thesis: verum
end;
hence A = B ; :: thesis: verum