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

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{1}[c] implies not P_{4}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{4}[c] ) & ( P_{3}[c] implies not P_{4}[c] ) )
by A1;

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

A4: for r being Element of F_{1}() holds

( r in dom f iff ( P_{1}[r] or P_{2}[r] or P_{3}[r] or P_{4}[r] ) )
and

A5: for o being Element of F_{1}() st o in dom f holds

( ( P_{1}[o] implies f . o = F_{3}(o) ) & ( P_{2}[o] implies f . o = F_{4}(o) ) & ( P_{3}[o] implies f . o = F_{5}(o) ) & ( P_{4}[o] implies f . o = F_{6}(o) ) )
from SCHEME1:sch 11(A3);

set q = f;

A6: dom f = F_{1}()
_{1}(),F_{2}() by FUNCT_2:def 1;

take q ; :: thesis: for c being Element of F_{1}() holds

( ( P_{1}[c] implies q . c = F_{3}(c) ) & ( P_{2}[c] implies q . c = F_{4}(c) ) & ( P_{3}[c] implies q . c = F_{5}(c) ) & ( P_{4}[c] implies q . c = F_{6}(c) ) )

let e be Element of F_{1}(); :: thesis: ( ( P_{1}[e] implies q . e = F_{3}(e) ) & ( P_{2}[e] implies q . e = F_{4}(e) ) & ( P_{3}[e] implies q . e = F_{5}(e) ) & ( P_{4}[e] implies q . e = F_{6}(e) ) )

thus ( ( P_{1}[e] implies q . e = F_{3}(e) ) & ( P_{2}[e] implies q . e = F_{4}(e) ) & ( P_{3}[e] implies q . e = F_{5}(e) ) & ( P_{4}[e] implies q . e = F_{6}(e) ) )
by A5, A6; :: thesis: verum

( ( P

consider f being PartFunc of F

A4: for r being Element of F

( r in dom f iff ( P

A5: for o being Element of F

( ( P

set q = f;

A6: dom f = F

proof

then reconsider q = f as Function 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 w9 = x as Element of F_{1}() ;

( P_{1}[w9] or P_{2}[w9] or P_{3}[w9] or P_{4}[w9] )
by A2;

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

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

assume x in F

then reconsider w9 = x as Element of F

( P

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

take q ; :: thesis: for c being Element of F

( ( P

let e be Element of F

thus ( ( P