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 set ; :: 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 set such that
A2: ( z in dom F₄() & z in { F₃(x) where x is Element of F₁() : P₁[x] } & y = F₄() . z ) by FUNCT_1:def 12;
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 A2; :: thesis: verum

end;

let y be set ; :: 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
A3: ( y = F₄() . F₃(x) & P₁[x] ) ;
F₃(x) in the carrier of F₂() ;
then ( F₃(x) in dom F₄() & F₃(x) in { F₃(z) where z is Element of F₁() : P₁[z] } ) by A1, A3;
hence y in F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } by A3, FUNCT_1:def 12; :: thesis: verum