let X, Y be set ; :: thesis: for f1, f2 being Function st rng f1 c= Funcs X,Y & rng f2 c= Funcs X,Y & X <> {} & uncurry' f1 = uncurry' f2 holds
f1 = f2
let f1, f2 be Function; :: thesis: ( rng f1 c= Funcs X,Y & rng f2 c= Funcs X,Y & X <> {} & uncurry' f1 = uncurry' f2 implies f1 = f2 )
assume A1: ( rng f1 c= Funcs X,Y & rng f2 c= Funcs X,Y & X <> {} & uncurry' f1 = uncurry' f2 ) ; :: thesis: f1 = f2
then ( dom (uncurry f1) = [:(dom f1),X:] & dom (uncurry f2) = [:(dom f2),X:] ) by Th33;
then ( uncurry f1 = ~ (~ (uncurry f1)) & uncurry f2 = ~ (~ (uncurry f2)) & uncurry' f1 = ~ (uncurry f1) & uncurry' f2 = ~ (uncurry f2) ) by FUNCT_4:53;
hence f1 = f2 by A1, Th53; :: thesis: verum