A3: for c being Element of F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) by A1;
consider f being PartFunc of F1(),F2() such that
A4: for w being Element of F1() holds
( w in dom f iff ( P1[w] or P2[w] or P3[w] ) ) and
A5: for q being Element of F1() st q in dom f holds
( ( P1[q] implies f . q = F3(q) ) & ( P2[q] implies f . q = F4(q) ) & ( P3[q] implies f . q = F5(q) ) ) from SCHEME1:sch 9(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 t9 = x as Element of F1() ;
( P1[t9] or P2[t9] or P3[t9] ) 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) ) )
let t be Element of F1(); :: thesis: ( ( P1[t] implies q . t = F3(t) ) & ( P2[t] implies q . t = F4(t) ) & ( P3[t] implies q . t = F5(t) ) )
thus ( ( P1[t] implies q . t = F3(t) ) & ( P2[t] implies q . t = F4(t) ) & ( P3[t] implies q . t = F5(t) ) ) by A5, A6; :: thesis: verum