set f = F5();
thus F5() .: { F4(x) where x is Element of F1() : P1[x] } c= { (F5() . F4(x)) where x is Element of F2() : P1[x] } :: according to XBOOLE_0:def 10 :: thesis: { (F5() . F4(x)) where x is Element of F2() : P1[x] } c= F5() .: { F4(x) where x is Element of F1() : P1[x] }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F5() .: { F4(x) where x is Element of F1() : P1[x] } or y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } )
assume y in F5() .: { F4(x) where x is Element of F1() : P1[x] } ; :: thesis: y in { (F5() . F4(x)) where x is Element of F2() : P1[x] }
then consider z being object such that
z in dom F5() and
A3: z in { F4(x) where x is Element of F1() : P1[x] } and
A4: y = F5() . z by FUNCT_1:def 6;
consider x being Element of F1() such that
A5: z = F4(x) and
A6: P1[x] by A3;
reconsider x = x as Element of F2() by A2;
y = F5() . F4(x) by A4, A5;
hence y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } by A6; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } or y in F5() .: { F4(x) where x is Element of F1() : P1[x] } )
assume y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } ; :: thesis: y in F5() .: { F4(x) where x is Element of F1() : P1[x] }
then consider x being Element of F2() such that
A7: y = F5() . F4(x) and
A8: P1[x] ;
reconsider x = x as
Element of F1() by A2;
A9: F4(x) in the carrier of F3() ;
F4(x) in { F4(z) where z is Element of F1() : P1[z] } by A8;
hence y in F5() .: { F4(x) where x is Element of F1() : P1[x] } by ; :: thesis: verum