set D = { a where a is Element of F3() : ( P1[a] or P2[a] ) } ;
per cases ( { a where a is Element of F3() : ( P1[a] or P2[a] ) } = {} or { a where a is Element of F3() : ( P1[a] or P2[a] ) } <> {} ) ;
suppose A3: { a where a is Element of F3() : ( P1[a] or P2[a] ) } = {} ; :: thesis: ex f being Function of F3(),F2() st
for a being Element of F1() st a in F3() holds
( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) )
consider f being Function such that
A4: ( dom f = F3() & ( for u being object st u in F3() holds
f . u = F6(u) ) ) from FUNCT_1:sch 3();
 rng f c= F2()
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in rng f or v in F2() )
assume v in rng f ; :: thesis: v in F2()
then consider u being object such that
A5: u in dom f and
A6: v = f . u by FUNCT_1:def 3;
A7: v = F6(u) by A4, A5, A6;
A8: not u in { a where a is Element of F3() : ( P1[a] or P2[a] ) } by A3;
then A9: P2[u] by A4, A5;
P1[u] by A8, A4, A5;
hence v in F2() by A9, A7, A1, A2, A4, A5; :: thesis: verum
end;
then reconsider f = f as Function of F3(),F2() by A4, FUNCT_2:2;
take f ; :: thesis: for a being Element of F1() st a in F3() holds
( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) )
let a be Element of F1(); :: thesis: ( a in F3() implies ( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) ) )
assume A10: a in F3() ; :: thesis: ( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) )
not a in { a where a is Element of F3() : ( P1[a] or P2[a] ) } by A3;
hence ( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) ) by A4, A10; :: thesis: verum
end;
suppose { a where a is Element of F3() : ( P1[a] or P2[a] ) } <> {} ; :: thesis: ex f being Function of F3(),F2() st
for a being Element of F1() st a in F3() holds
( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) )
then reconsider D = { a where a is Element of F3() : ( P1[a] or P2[a] ) } as non empty set ;
defpred S1[ object ] means ( P1[$1] or P2[$1] );
A11: for a being object st a in D holds
( ( P1[a] implies F4(a) in F2() ) & ( P1[a] implies F5(a) in F2() ) )
proof
let a be object ; :: thesis: ( a in D implies ( ( P1[a] implies F4(a) in F2() ) & ( P1[a] implies F5(a) in F2() ) ) )
assume a in D ; :: thesis: ( ( P1[a] implies F4(a) in F2() ) & ( P1[a] implies F5(a) in F2() ) )
then A12: ex b being Element of F3() st
( a = b & ( P1[b] or P2[b] ) ) ;
then a in F3() ;
hence ( ( P1[a] implies F4(a) in F2() ) & ( P1[a] implies F5(a) in F2() ) ) by A12, A1, A2; :: thesis: verum
end;
consider g being Function of D,F2() such that
A13: for x being object st x in D holds
( ( P1[x] implies g . x = F4(x) ) & ( P1[x] implies g . x = F5(x) ) ) from FUNCT_2:sch 5(A11);
deffunc H1( object ) -> set = g . $1;
A14: for a being object st a in F3() holds
( ( S1[a] implies H1(a) in F2() ) & ( not S1[a] implies F6(a) in F2() ) )
proof
let a be object ; :: thesis: ( a in F3() implies ( ( S1[a] implies H1(a) in F2() ) & ( not S1[a] implies F6(a) in F2() ) ) )
assume A15: a in F3() ; :: thesis: ( ( S1[a] implies H1(a) in F2() ) & ( not S1[a] implies F6(a) in F2() ) )
hereby :: thesis: ( not S1[a] implies F6(a) in F2() )
assume S1[a] ; :: thesis: H1(a) in F2()
then A16: a in D by A15;
then A17: ( P1[a] implies F5(a) in F2() ) by A11;
( P1[a] implies F4(a) in F2() ) by A16, A11;
hence H1(a) in F2() by A17, A16, A13; :: thesis: verum
end;
thus ( not S1[a] implies F6(a) in F2() ) by A1, A2, A15; :: thesis: verum
end;
consider f being Function of F3(),F2() such that
A18: for x being object st x in F3() holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = F6(x) ) ) from FUNCT_2:sch 5(A14);
take f ; :: thesis: for a being Element of F1() st a in F3() holds
( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) )
let a be Element of F1(); :: thesis: ( a in F3() implies ( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) ) )
assume A19: a in F3() ; :: thesis: ( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) & ( P1[a] & P2[a] implies f . a = F6(a) ) )
then ( S1[a] implies ( f . a = g . a & a in D ) ) by A18;
hence ( ( P1[a] implies f . a = F4(a) ) & ( P1[a] & P2[a] implies f . a = F5(a) ) ) by A13; :: thesis: ( P1[a] & P2[a] implies f . a = F6(a) )
thus ( P1[a] & P2[a] implies f . a = F6(a) ) by A18, A19; :: thesis: verum
end;
end;