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