let f be non-empty Function; 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 ; 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 ; ( 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))
; ( 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
X = Y
thus X =
(f +* (j,Y)) . i
by A1, A4, FUNCT_7:31
.=
Y
by A1, A5, FUNCT_7:31
; verum