A3: for c being Element of F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) by A1;
consider f being PartFunc of F1(),F2() such that
A4: for r being Element of F1() holds
( r in dom f iff ( P1[r] or P2[r] or P3[r] or P4[r] ) ) and
A5: for o being Element of F1() st o in dom f holds
( ( P1[o] implies f . o = F3(o) ) & ( P2[o] implies f . o = F4(o) ) & ( P3[o] implies f . o = F5(o) ) & ( P4[o] implies f . o = F6(o) ) ) from SCHEME1:sch 11(A3);
 set q = f;
A6: dom f = F1()
proof
thus dom f c= F1() ; :: according to XBOOLE_0:def 10 :: thesis: F1() c= dom f
let x be set ; :: 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 w9 = x as Element of F1() ;
( P1[w9] or P2[w9] or P3[w9] or P4[w9] ) by A2;
hence x in dom f by A4; :: thesis: verum
end;
then reconsider q = f as Function of F1(),F2() by FUNCT_2:def 1;
take q ; :: thesis: for c being Element of F1() holds
( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) & ( P4[c] implies q . c = F6(c) ) )
let e be Element of F1(); :: thesis: ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) & ( P3[e] implies q . e = F5(e) ) & ( P4[e] implies q . e = F6(e) ) )
thus ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) & ( P3[e] implies q . e = F5(e) ) & ( P4[e] implies q . e = F6(e) ) ) by A5, A6; :: thesis: verum