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 SCHEME1:sch 6(A1);
take
f
; ( 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()
hence
f is total
by PARTFUN1:def 2; 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; verum