let f be non-empty Function; :: thesis: for X, Y being non empty set

for i, j being object st i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) holds

( i = j & X c= Y )

let X, Y be non empty set ; :: thesis: for i, j being object st i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) holds

( i = j & X c= Y )

let i, j be object ; :: thesis: ( i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) implies ( i = j & X c= Y ) )

assume that

A1: ( i in dom f & j in dom f ) and

A2: ( not X c= f . i or not f . j c= Y ) and

A3: product (f +* (i,X)) c= product (f +* (j,Y)) ; :: thesis: ( i = j & X c= Y )

a4: ( f +* (i,X) is non-empty & f +* (j,Y) is non-empty ) by A1, Th35;

thus A5: i = j :: thesis: X c= Y

assume A9: x in X ; :: thesis: x in Y

set g = the Element of product f;

A10: the Element of product f +* (i,x) in product (f +* (i,X)) by A1, A9, Th37;

i in dom (f +* (j,Y)) by A1, FUNCT_7:30;

then ( the Element of product f +* (i,x)) . i in (f +* (j,Y)) . i by A3, A10, CARD_3:9;

then A11: ( the Element of product f +* (i,x)) . i in Y by A1, A5, FUNCT_7:31;

i in dom the Element of product f by A1, CARD_3:9;

hence x in Y by A11, FUNCT_7:31; :: thesis: verum

for i, j being object st i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) holds

( i = j & X c= Y )

let X, Y be non empty set ; :: thesis: for i, j being object st i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) holds

( i = j & X c= Y )

let i, j be object ; :: thesis: ( i in dom f & j in dom f & ( not X c= f . i or not f . j c= Y ) & product (f +* (i,X)) c= product (f +* (j,Y)) implies ( i = j & X c= Y ) )

assume that

A1: ( i in dom f & j in dom f ) and

A2: ( not X c= f . i or not f . j c= Y ) and

A3: product (f +* (i,X)) c= product (f +* (j,Y)) ; :: thesis: ( i = j & X c= Y )

a4: ( f +* (i,X) is non-empty & f +* (j,Y) is non-empty ) by A1, Th35;

thus A5: i = j :: thesis: X c= Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A6:
i <> j
; :: thesis: contradiction

A7: ( i in dom (f +* (i,X)) & j in dom (f +* (i,X)) ) by A1, FUNCT_7:30;

(f +* (i,X)) . i c= (f +* (j,Y)) . i by a4, A7, A3, PUA2MSS1:1;

then a8: X c= (f +* (j,Y)) . i by A1, FUNCT_7:31;

(f +* (i,X)) . j c= (f +* (j,Y)) . j by a4, A7, A3, PUA2MSS1:1;

then (f +* (i,X)) . j c= Y by A1, FUNCT_7:31;

hence contradiction by A2, a8, A6, FUNCT_7:32; :: thesis: verum

end;A7: ( i in dom (f +* (i,X)) & j in dom (f +* (i,X)) ) by A1, FUNCT_7:30;

(f +* (i,X)) . i c= (f +* (j,Y)) . i by a4, A7, A3, PUA2MSS1:1;

then a8: X c= (f +* (j,Y)) . i by A1, FUNCT_7:31;

(f +* (i,X)) . j c= (f +* (j,Y)) . j by a4, A7, A3, PUA2MSS1:1;

then (f +* (i,X)) . j c= Y by A1, FUNCT_7:31;

hence contradiction by A2, a8, A6, FUNCT_7:32; :: thesis: verum

assume A9: x in X ; :: thesis: x in Y

set g = the Element of product f;

A10: the Element of product f +* (i,x) in product (f +* (i,X)) by A1, A9, Th37;

i in dom (f +* (j,Y)) by A1, FUNCT_7:30;

then ( the Element of product f +* (i,x)) . i in (f +* (j,Y)) . i by A3, A10, CARD_3:9;

then A11: ( the Element of product f +* (i,x)) . i in Y by A1, A5, FUNCT_7:31;

i in dom the Element of product f by A1, CARD_3:9;

hence x in Y by A11, FUNCT_7:31; :: thesis: verum