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
A3: ( z in dom F₅() & z in { F₄(x) where x is Element of F₁() : P₁[x] } & y = F₅() . z ) by FUNCT_1:def 12;
consider x being Element of F₁() such that
A4: ( z = F₄(x) & P₁[x] ) by A3;
reconsider x = x as Element of F₂() by A2;
( y = F₅() . F₄(x) & P₁[x] ) by A3, A4;
hence y in { (F₅() . F₄(x)) where x is Element of F₂() : P₁[x] } ; :: 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
A5: ( y = F₅() . F₄(x) & P₁[x] ) ;
reconsider x = x as Element of F₁() by A2;
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, A5;
hence y in F₅() .: { F₄(x) where x is Element of F₁() : P₁[x] } by A5, FUNCT_1:def 12; :: thesis: verum