let A, B, C be set ; :: thesis: ( ( B = {} implies A = {} ) implies for f being Function of A, Funcs B,C
for g being Function of A,B holds rng (f .. g) c= C )
assume A1: ( B = {} implies A = {} ) ; :: thesis: for f being Function of A, Funcs B,C
for g being Function of A,B holds rng (f .. g) c= C
let f be Function of A, Funcs B,C; :: thesis: for g being Function of A,B holds rng (f .. g) c= C
let g be Function of A,B; :: thesis: rng (f .. g) c= C
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f .. g) or x in C )
assume x in rng (f .. g) ; :: thesis: x in C
then consider y being set such that
A2: y in dom (f .. g) and
A3: (f .. g) . y = x by FUNCT_1:def 5;
A4: dom (f .. g) = dom f by PRALG_1:def 17;
then A5: rng f <> {} by A2, RELAT_1:60, RELAT_1:64;
rng f c= Funcs B,C by RELSET_1:12;
then A6: Funcs B,C <> {} by A5;
then A7: dom f = A by FUNCT_2:def 1;
then reconsider fy = f . y as Function of B,C by A2, A4, A6, FUNCT_2:7, FUNCT_2:121;
A8: C <> {} by A1, A2, A6, A7, PRALG_1:def 17;
g . y in B by A1, A2, A4, A7, FUNCT_2:7;
then fy . (g . y) in C by A8, FUNCT_2:7;
hence x in C by A2, A3, A4, PRALG_1:def 17; :: thesis: verum