set f = F_{5}();

thus F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] } c= { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] }
:: according to XBOOLE_0:def 10 :: thesis: { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] } c= F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] } _{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] } or y in F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] } )

assume y in { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] }
; :: thesis: y in F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] }

then consider x being Element of F_{2}() such that

A7: y = F_{5}() . F_{4}(x)
and

A8: P_{1}[x]
;

reconsider x = x as Element of F_{1}() by A2;

A9: F_{4}(x) in the carrier of F_{3}()
;

F_{4}(x) in { F_{4}(z) where z is Element of F_{1}() : P_{1}[z] }
by A8;

hence y in F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] }
by A1, A7, A9, FUNCT_1:def 6; :: thesis: verum

thus F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (F
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] } or y in { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] } )

assume y in F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] }
; :: thesis: y in { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] }

then consider z being object such that

z in dom F_{5}()
and

A3: z in { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] }
and

A4: y = F_{5}() . z
by FUNCT_1:def 6;

consider x being Element of F_{1}() such that

A5: z = F_{4}(x)
and

A6: P_{1}[x]
by A3;

reconsider x = x as Element of F_{2}() by A2;

y = F_{5}() . F_{4}(x)
by A4, A5;

hence y in { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] }
by A6; :: thesis: verum

end;assume y in F

then consider z being object such that

z in dom F

A3: z in { F

A4: y = F

consider x being Element of F

A5: z = F

A6: P

reconsider x = x as Element of F

y = F

hence y in { (F

assume y in { (F

then consider x being Element of F

A7: y = F

A8: P

reconsider x = x as Element of F

A9: F

F

hence y in F