let X1, X2, Y1, Y2 be set ; ( X1 c= X2 & Y1 c= Y2 implies PFuncs (X1,Y1) c= PFuncs (X2,Y2) )
assume A1:
( X1 c= X2 & Y1 c= Y2 )
; PFuncs (X1,Y1) c= PFuncs (X2,Y2)
let f be object ; TARSKI:def 3 ( not f in PFuncs (X1,Y1) or f in PFuncs (X2,Y2) )
assume
f in PFuncs (X1,Y1)
; f in PFuncs (X2,Y2)
then
f is PartFunc of X1,Y1
by Th46;
then
f is PartFunc of X2,Y2
by A1, RELSET_1:7;
hence
f in PFuncs (X2,Y2)
by Th45; verum