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_{2}[c] implies not P_{3}[c] ) )
by A1;

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

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

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

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

( ( P_{1}[q] implies f . q = F_{3}(q) ) & ( P_{2}[q] implies f . q = F_{4}(q) ) & ( P_{3}[q] implies f . q = F_{5}(q) ) )
from SCHEME1:sch 9(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) ) )

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

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

( ( P

consider f being PartFunc of F

A4: for w being Element of F

( w in dom f iff ( P

A5: for q 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 t9 = x as Element of F_{1}() ;

( P_{1}[t9] or P_{2}[t9] or P_{3}[t9] )
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 t9 = 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 t be Element of F

thus ( ( P