let X, Y be set ; 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; ( 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
; ( 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; verum