let X1, X2, Y1, Y2 be set ; :: thesis: ( X1 c= X2 & Y1 c= Y2 implies PFuncs X1,Y1 c= PFuncs X2,Y2 )
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis: PFuncs X1,Y1 c= PFuncs X2,Y2
let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in PFuncs X1,Y1 or f in PFuncs X2,Y2 )
assume f in PFuncs X1,Y1 ; :: thesis: f in PFuncs X2,Y2
then f is PartFunc of X1,Y1 by Th120;
then f is PartFunc of X2,Y2 by A1, RELSET_1:17;
hence f in PFuncs X2,Y2 by Th119; :: thesis: verum