defpred S_{1}[ set ] means P_{1}[$1];

A1: for c being Element of F_{1}() st P_{1}[c] holds

not S_{1}[c]
;

consider f being PartFunc of F_{1}(),F_{2}() such that

A2: ( ( for c being Element of F_{1}() holds

( c in dom f iff ( P_{1}[c] or S_{1}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( S_{1}[c] implies f . c = F_{4}(c) ) ) ) )
from SCHEME1:sch 6(A1);

take f ; :: thesis: ( f is total & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{1}[c] implies f . c = F_{4}(c) ) ) ) )

dom f = F_{1}()
_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{1}[c] implies f . c = F_{4}(c) ) )

thus for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{1}[c] implies f . c = F_{4}(c) ) )
by A2; :: thesis: verum

A1: for c being Element of F

not S

consider f being PartFunc of F

A2: ( ( for c being Element of F

( c in dom f iff ( P

( ( P

take f ; :: thesis: ( f is total & ( for c being Element of F

( ( P

dom f = F

proof

hence
f is total
by PARTFUN1:def 2; :: thesis: for c being Element of F
thus
dom f c= F_{1}()
; :: according to XBOOLE_0:def 10 :: thesis: F_{1}() c= dom f

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F_{1}() or x in dom f )

assume x in F_{1}()
; :: thesis: x in dom f

then reconsider b9 = x as Element of F_{1}() ;

( P_{1}[b9] or not P_{1}[b9] )
;

hence x in dom f by A2; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F

assume x in F

then reconsider b9 = x as Element of F

( P

hence x in dom f by A2; :: thesis: verum

( ( P

thus for c being Element of F

( ( P