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 & ( X <> f . i or Y <> f . j ) & product (f +* (i,X)) = product (f +* (j,Y)) holds

( i = j & X = Y )

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

( i = j & X = Y )

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

assume that

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

A2: ( X <> f . i or Y <> f . j ) and

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

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

then A4: f +* (i,X) = f +* (j,Y) by A3, PUA2MSS1:2;

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

.= Y by A1, A5, FUNCT_7:31 ; :: thesis: verum

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

( i = j & X = Y )

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

( i = j & X = Y )

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

assume that

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

A2: ( X <> f . i or Y <> f . j ) and

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

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

then A4: f +* (i,X) = f +* (j,Y) by A3, PUA2MSS1:2;

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

proof

thus X =
(f +* (j,Y)) . i
by A1, A4, FUNCT_7:31
assume A6:
i <> j
; :: thesis: contradiction

A7: X = (f +* (i,X)) . i by A1, FUNCT_7:31

.= f . i by A4, A6, FUNCT_7:32 ;

Y = (f +* (j,Y)) . j by A1, FUNCT_7:31

.= f . j by A4, A6, FUNCT_7:32 ;

hence contradiction by A2, A7; :: thesis: verum

end;A7: X = (f +* (i,X)) . i by A1, FUNCT_7:31

.= f . i by A4, A6, FUNCT_7:32 ;

Y = (f +* (j,Y)) . j by A1, FUNCT_7:31

.= f . j by A4, A6, FUNCT_7:32 ;

hence contradiction by A2, A7; :: thesis: verum

.= Y by A1, A5, FUNCT_7:31 ; :: thesis: verum