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 ( dom (~ f1) = [:Y,X:] & dom (~ f2) = [:Y,X:] & curry' f1 = curry (~ f1) & curry' f2 = curry (~ f2) ) by FUNCT_4:47;
then ( ~ f1 = ~ f2 & ~ (~ f1) = f1 & ~ (~ f2) = f2 ) by A1, Th51, FUNCT_4:53;
hence f1 = f2 ; :: thesis: verum