consider fs being Subset of (PFuncs (F_{1}(),F_{2}())) such that

A1: for f being set holds

( f in fs iff ( f in PFuncs (F_{1}(),F_{2}()) & P_{1}[f] ) )
from SUBSET_1:sch 1();

take fs ; :: thesis: for pfs being PartFunc of F_{1}(),F_{2}() holds

( pfs in fs iff P_{1}[pfs] )

let pfs be PartFunc of F_{1}(),F_{2}(); :: thesis: ( pfs in fs iff P_{1}[pfs] )

pfs in PFuncs (F_{1}(),F_{2}())
by PARTFUN1:45;

hence ( pfs in fs iff P_{1}[pfs] )
by A1; :: thesis: verum

A1: for f being set holds

( f in fs iff ( f in PFuncs (F

take fs ; :: thesis: for pfs being PartFunc of F

( pfs in fs iff P

let pfs be PartFunc of F

pfs in PFuncs (F

hence ( pfs in fs iff P