A3: for c being set holds
( not c in F1() or P1[c] or P2[c] or P3[c] ) by A2;
A4: for c being set st c in F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) by A1;
ex f being Function st
( dom f = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) ) ) from RECDEF_2:sch 1(A4, A3);
 then consider f being Function such that
A5: dom f = F1() and
A6: for c being set st c in F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) ;
take f ; :: thesis: ( dom f = F1() & ( for c being Element of F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) ) )
thus dom f = F1() by A5; :: thesis: for c being Element of F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) )
let c be Element of F1(); :: thesis: ( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) )
thus ( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) by A6; :: thesis: verum