consider fs being Subset of (PFuncs F1(),F2()) such that
A1:
for f being set holds
( f in fs iff ( f in PFuncs F1(),F2() & P1[f] ) )
from SUBSET_1:sch 1();
take
fs
; :: thesis: for pfs being PartFunc of F1(),F2() holds
( pfs in fs iff P1[pfs] )
let pfs be PartFunc of F1(),F2(); :: thesis: ( pfs in fs iff P1[pfs] )
pfs in PFuncs F1(),F2()
by PARTFUN1:119;
hence
( pfs in fs iff P1[pfs] )
by A1; :: thesis: verum