defpred S₁[ object , object ] means ( ( P₁[$1] & $2 = TRUE ) or ( P₁[$1] & $2 = FALSE ) );
A2: for d being object st d in F₂() holds
ex z being object st
( z in BOOLEAN & S₁[d,z] )

proof

let d be object ; :: thesis: ( d in F₂() implies ex z being object st
( z in BOOLEAN & S₁[d,z] ) )
assume d in F₂() ; :: thesis: ex z being object st
( z in BOOLEAN & S₁[d,z] )

per cases ( S₁[d, TRUE ] or S₁[d, FALSE ] ) ;

suppose A3: S₁[d, TRUE ] ; :: thesis: ex z being object st
( z in BOOLEAN & S₁[d,z] )

take TRUE ; :: thesis: ( TRUE in BOOLEAN & S₁[d, TRUE ] )
thus ( TRUE in BOOLEAN & S₁[d, TRUE ] ) by A3; :: thesis: verum

end;

suppose A4: S₁[d, FALSE ] ; :: thesis: ex z being object st
( z in BOOLEAN & S₁[d,z] )

take FALSE ; :: thesis: ( FALSE in BOOLEAN & S₁[d, FALSE ] )
thus ( FALSE in BOOLEAN & S₁[d, FALSE ] ) by A4; :: thesis: verum

end;

end;

end;

consider p being Function of F₂(),BOOLEAN such that
A5: for d being object st d in F₂() holds
S₁[d,p . d] from FUNCT_2:sch 1(A2);
A6: p in PFuncs (F₂(),BOOLEAN) by PARTFUN1:45;
PFuncs (F₂(),BOOLEAN) c= PFuncs (F₁(),BOOLEAN) by A1, PARTFUN1:50;
then reconsider p = p as PartialPredicate of F₁() by A6, PARTFUN1:46;
take p ; :: thesis: ( dom p = F₂() & ( for d being object st d in dom p holds
( ( P₁[d] implies p . d = TRUE ) & ( P₁[d] implies p . d = FALSE ) ) ) )
dom p = F₂() by FUNCT_2:def 1;
hence ( dom p = F₂() & ( for d being object st d in dom p holds
( ( P₁[d] implies p . d = TRUE ) & ( P₁[d] implies p . d = FALSE ) ) ) ) by A5; :: thesis: verum