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 object ; :: 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 Th46;
then f is PartFunc of X2,Y2 by A1, RELSET_1:7;
hence f in PFuncs (X2,Y2) by Th45; :: thesis: verum