let X, Y be set ; :: thesis: for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds
f1 = f2
let f1, f2 be Function; :: thesis: ( dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2 )
assume ( dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] ) ; :: thesis: ( not curry' f1 = curry' f2 or f1 = f2 )
then ( uncurry' (curry' f1) = f1 & uncurry' (curry' f2) = f2 ) by Th57;
hence ( not curry' f1 = curry' f2 or f1 = f2 ) ; :: thesis: verum