set f = F_{4}();

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

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

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

A4: y = F_{4}() . F_{3}(x)
and

A5: P_{1}[x]
;

A6: F_{3}(x) in the carrier of F_{2}()
;

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

hence y in F_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] }
by A1, A4, A6, 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_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] } or y in { (F_{4}() . F_{3}(x)) where x is Element of F_{1}() : P_{1}[x] } )

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

then consider z being object such that

z in dom F_{4}()
and

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

A3: y = F_{4}() . z
by FUNCT_1:def 6;

ex x being Element of F_{1}() st

( z = F_{3}(x) & P_{1}[x] )
by A2;

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

end;assume y in F

then consider z being object such that

z in dom F

A2: z in { F

A3: y = F

ex x being Element of F

( z = F

hence y in { (F

assume y in { (F

then consider x being Element of F

A4: y = F

A5: P

A6: F

F

hence y in F