defpred S1[ set ] means P1[\$1];
A1: for c being Element of F1() st P1[c] holds
not S1[c] ;
consider f being PartFunc of F1(),F2() such that
A2: ( ( for c being Element of F1() holds
( c in dom f iff ( P1[c] or S1[c] ) ) ) & ( for c being Element of F1() st c in dom f holds
( ( P1[c] implies f . c = F3(c) ) & ( S1[c] implies f . c = F4(c) ) ) ) ) from take f ; :: thesis: ( f is total & ( for c being Element of F1() st c in dom f holds
( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) ) )

dom f = F1()
proof
thus dom f c= F1() ; :: according to XBOOLE_0:def 10 :: thesis: F1() c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1() or x in dom f )
assume x in F1() ; :: thesis: x in dom f
then reconsider b9 = x as Element of F1() ;
( P1[b9] or not P1[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 F1() st c in dom f holds
( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) )

thus for c being Element of F1() st c in dom f holds
( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) by A2; :: thesis: verum