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

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

hence
A = B
; :: thesis: verumA . 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;

A7: dom F = I by PARTFUN1:def 2;

then f . (A . i) = (F .. A) . i by A4, PRALG_1:def 17

.= f . (B . i) by A3, A4, A7, PRALG_1:def 17 ;

hence A . i = B . i by A5, A6; :: thesis: verum

end;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;

A7: dom F = I by PARTFUN1:def 2;

then f . (A . i) = (F .. A) . i by A4, PRALG_1:def 17

.= f . (B . i) by A3, A4, A7, PRALG_1:def 17 ;

hence A . i = B . i by A5, A6; :: thesis: verum