set f = F₄();
thus F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } c= { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] } :: according to XBOOLE_0:def 10 :: thesis: { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] } c= F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } or y in { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] } )
assume y in F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } ; :: thesis: y in { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] }
then consider z being object such that
z in dom F₄() and
A2: z in { F₃(x) where x is Element of F₁() : P₁[x] } and
A3: y = F₄() . z by FUNCT_1:def 6;
ex x being Element of F₁() st
( z = F₃(x) & P₁[x] ) by A2;
hence y in { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] } by A3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] } or y in F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } )
assume y in { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] } ; :: thesis: y in F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] }
then consider x being Element of F₁() such that
A4: y = F₄() . F₃(x) and
A5: P₁[x] ;
( F₃(x) in the carrier of F₂() & F₃(x) in { F₃(z) where z is Element of F₁() : P₁[z] } ) by A5;
hence y in F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } by A1, A4, FUNCT_1:def 6; :: thesis: verum