let A be set ; :: thesis: for B, C being non empty set
for f being Function of A,B
for g being Function of B,C st rng (g * f) = C holds
rng g = C
let B, C be non empty set ; :: thesis: for f being Function of A,B
for g being Function of B,C st rng (g * f) = C holds
rng g = C
let f be Function of A,B; :: thesis: for g being Function of B,C st rng (g * f) = C holds
rng g = C
let g be Function of B,C; :: thesis: ( rng (g * f) = C implies rng g = C )
assume A1: rng (g * f) = C ; :: thesis: rng g = C
thus rng g c= C ; :: according to XBOOLE_0:def 10 :: thesis: C c= rng g
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in C or q in rng g )
assume q in C ; :: thesis: q in rng g
then consider x being set such that
A2: x in dom (g * f) and
A3: q = (g * f) . x by A1, FUNCT_1:def 5;
A4: dom f = A by FUNCT_2:def 1;
then A5: f . x in rng f by A2, FUNCT_1:def 5;
dom (g * f) = A by FUNCT_2:def 1;
then A6: rng f c= dom g by A4, FUNCT_1:27;
q = g . (f . x) by A2, A3, FUNCT_1:22;
hence q in rng g by A6, A5, FUNCT_1:def 5; :: thesis: verum