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
A3: z in { F₄(x) where x is Element of F₁() : P₁[x] } and
A4: y = F₅() . z by FUNCT_1:def 6;
consider x being Element of F₁() such that
A5: z = F₄(x) and
A6: P₁[x] by A3;
reconsider x = x as Element of F₂() by A2;
y = F₅() . F₄(x) by A4, A5;
hence y in { (F₅() . F₄(x)) where x is Element of F₂() : P₁[x] } by A6; :: 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
A7: y = F₅() . F₄(x) and
A8: P₁[x] ;
reconsider x = x as Element of F₁() by A2;
A9: F₄(x) in the carrier of F₃() ;
F₄(x) in { F₄(z) where z is Element of F₁() : P₁[z] } by A8;
hence y in F₅() .: { F₄(x) where x is Element of F₁() : P₁[x] } by A1, A7, A9, FUNCT_1:def 6; :: thesis: verum