let X, Y be set ; :: thesis: for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds
f1 = f2
let f1, f2 be Function; :: thesis: ( rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 implies f1 = f2 )
assume that
A1: rng f1 c= PFuncs (X,Y) and
A2: rng f2 c= PFuncs (X,Y) and
A3: not {} in rng f1 and
A4: not {} in rng f2 ; :: thesis: ( not uncurry' f1 = uncurry' f2 or f1 = f2 )
curry' (uncurry' f1) = f1 by A1, A3, Th44;
hence ( not uncurry' f1 = uncurry' f2 or f1 = f2 ) by A2, A4, Th44; :: thesis: verum