let X, Y be set ; :: thesis: for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds
f1 = f2
let f1, f2 be Function; :: thesis: ( dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 implies f1 = f2 )
assume A1:
( dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 )
; :: thesis: f1 = f2
then A2:
( [:X,Y:] = {} implies ( f1 = {} & f2 = {} ) )
;
now assume
[:X,Y:] <> {}
;
:: thesis: f1 = f2now let z be
set ;
:: thesis: ( z in [:X,Y:] implies f1 . z = f2 . z )assume
z in [:X,Y:]
;
:: thesis: f1 . z = f2 . zthen A4:
(
z = [(z `1 ),(z `2 )] &
z `1 in X &
z `2 in Y )
by MCART_1:10, MCART_1:23;
then consider g1 being
Function such that A5:
(
(curry f1) . (z `1 ) = g1 &
dom g1 = Y &
rng g1 c= rng f1 )
and A6:
for
y being
set st
y in Y holds
g1 . y = f1 . (z `1 ),
y
by A1, Th36;
consider g2 being
Function such that A7:
(
(curry f2) . (z `1 ) = g2 &
dom g2 = Y &
rng g2 c= rng f2 )
and A8:
for
y being
set st
y in Y holds
g2 . y = f2 . (z `1 ),
y
by A1, A4, Th36;
A9:
f1 . (z `1 ),
(z `2 ) = g1 . (z `2 )
by A4, A6;
f2 . (z `1 ),
(z `2 ) = g1 . (z `2 )
by A1, A4, A5, A7, A8;
hence
f1 . z = f2 . z
by A4, A9;
:: thesis: verum end; hence
f1 = f2
by A1, FUNCT_1:9;
:: thesis: verum end;
hence
f1 = f2
by A2; :: thesis: verum