let Y be set ; :: thesis: for f, g being Function st Y c= rng g & g " Y c= rng f holds
Y c= rng (g * f)
let f, g be Function; :: thesis: ( Y c= rng g & g " Y c= rng f implies Y c= rng (g * f) )
assume that
A1: Y c= rng g and
A2: g " Y c= rng f ; :: thesis: Y c= rng (g * f)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng (g * f) )
assume A3: y in Y ; :: thesis: y in rng (g * f)
then consider z being object such that
A4: ( z in dom g & y = g . z ) by A1, FUNCT_1:def 3;
z in g " Y by A3, A4, FUNCT_1:def 7;
then consider x being object such that
A5: ( x in dom f & z = f . x ) by A2, FUNCT_1:def 3;
( x in dom (g * f) & (g * f) . x = y ) by A4, A5, FUNCT_1:11, FUNCT_1:13;
hence y in rng (g * f) by FUNCT_1:def 3; :: thesis: verum