A2: now :: thesis: ( F2() = {} implies not F1() <> {} )
set x = the Element of F1();
assume A3: F2() = {} ; :: thesis: not F1() <> {}
assume A4: F1() <> {} ; :: thesis: contradiction
then ( P1[ the Element of F1()] implies F3( the Element of F1()) in F2() ) by A1;
hence contradiction by A1, A3, A4; :: thesis: verum
end;
consider f being Function such that
A5: dom f = F1() and
A6: for x being object st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) from PARTFUN1:sch 1();
 rng f c= F2()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in F2() )
assume y in rng f ; :: thesis: y in F2()
then consider x being object such that
A7: x in dom f and
A8: y = f . x by FUNCT_1:def 3;
A9: ( P1[x] implies f . x = F4(x) ) by A5, A6, A7;
( P1[x] implies f . x = F3(x) ) by A5, A6, A7;
hence y in F2() by A1, A5, A7, A8, A9; :: thesis: verum
end;
then f is Function of F1(),F2() by A5, A2, Def1, RELSET_1:4;
hence ex f being Function of F1(),F2() st
for x being object st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) by A6; :: thesis: verum