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 that
A1: dom f1 = [:X,Y:] and
A2: dom f2 = [:X,Y:] and
A3: curry f1 = curry f2 ; :: thesis: f1 = f2
A4: now :: thesis: ( [:X,Y:] <> {} implies f1 = f2 )
assume [:X,Y:] <> {} ; :: thesis: f1 = f2
now :: thesis: for z being object st z in [:X,Y:] holds
f1 . z = f2 . z
let z be object ; :: thesis: ( z in [:X,Y:] implies f1 . z = f2 . z )
assume A5: z in [:X,Y:] ; :: thesis: f1 . z = f2 . z
then consider g1 being Function such that
A6: (curry f1) . (z `1) = g1 and
dom g1 = Y and
rng g1 c= rng f1 and
A7: for y being object st y in Y holds
g1 . y = f1 . ((z `1),y) by A1, Th22, MCART_1:10;
A8: z = [(z `1),(z `2)] by A5, MCART_1:21;
A9: z `2 in Y by A5, MCART_1:10;
then A10: f1 . ((z `1),(z `2)) = g1 . (z `2) by A7;
ex g2 being Function st
( (curry f2) . (z `1) = g2 & dom g2 = Y & rng g2 c= rng f2 & ( for y being object st y in Y holds
g2 . y = f2 . ((z `1),y) ) ) by A2, A5, Th22, MCART_1:10;
then f2 . ((z `1),(z `2)) = g1 . (z `2) by A3, A9, A6;
hence f1 . z = f2 . z by A8, A10; :: thesis: verum
end;
hence f1 = f2 by A1, A2; :: thesis: verum
end;
( [:X,Y:] = {} implies ( f1 = {} & f2 = {} ) ) by A1, A2;
hence f1 = f2 by A4; :: thesis: verum