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