defpred S₁[ set ] means P₁[$1];
A1: for c being Element of F₁() st P₁[c] holds
not S₁[c] ;
consider f being PartFunc of F₁(),F₂() such that
A2: ( ( for c being Element of F₁() holds
( c in dom f iff ( P₁[c] or S₁[c] ) ) ) & ( for c being Element of F₁() st c in dom f holds
( ( P₁[c] implies f . c = F₃(c) ) & ( S₁[c] implies f . c = F₄(c) ) ) ) ) from SCHEME1:sch 6(A1);
take f ; :: thesis: ( f is total & ( for c being Element of F₁() st c in dom f holds
( ( P₁[c] implies f . c = F₃(c) ) & ( P₁[c] implies f . c = F₄(c) ) ) ) )
dom f = F₁()

proof

thus dom f c= F₁() ; :: according to XBOOLE_0:def 10 :: thesis: F₁() c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F₁() or x in dom f )
assume x in F₁() ; :: thesis: x in dom f
then reconsider b9 = x as Element of F₁() ;
( P₁[b9] or not P₁[b9] ) ;
hence x in dom f by A2; :: thesis: verum

end;

hence f is total by PARTFUN1:def 2; :: thesis: for c being Element of F₁() st c in dom f holds
( ( P₁[c] implies f . c = F₃(c) ) & ( P₁[c] implies f . c = F₄(c) ) )
thus for c being Element of F₁() st c in dom f holds
( ( P₁[c] implies f . c = F₃(c) ) & ( P₁[c] implies f . c = F₄(c) ) ) by A2; :: thesis: verum