let A, B, C be set ; :: thesis: ( ( B = {} implies A = {} ) & ( C = {} implies B = {} ) implies for f being Function of A,(Funcs (B,C))

for g being Function of A,B holds rng (f .. g) c= C )

assume that

A1: ( B = {} implies A = {} ) and

a1: ( C = {} implies B = {} ) ; :: 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 object ; :: 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 object such that

A2: y in dom (f .. g) and

A3: (f .. g) . y = x by FUNCT_1:def 3;

S1: dom f = dom g

.= dom f by S1 ;

then A5: Funcs (B,C) <> {} by A2;

then A6: dom f = A by FUNCT_2:def 1;

then reconsider fy = f . y as Function of B,C by A2, A4, A5, FUNCT_2:5, FUNCT_2:66;

A7: C <> {} by A1, A2, A4;

g . y in B by A1, A2, A4, A6, FUNCT_2:5;

then fy . (g . y) in C by A7, FUNCT_2:5;

hence x in C by A2, A3, PRALG_1:def 19; :: thesis: verum

for g being Function of A,B holds rng (f .. g) c= C )

assume that

A1: ( B = {} implies A = {} ) and

a1: ( C = {} implies B = {} ) ; :: 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 object ; :: 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 object such that

A2: y in dom (f .. g) and

A3: (f .. g) . y = x by FUNCT_1:def 3;

S1: dom f = dom g

proof
end;

A4: dom (f .. g) =
(dom f) /\ (dom g)
by PRALG_1:def 19
.= dom f by S1 ;

then A5: Funcs (B,C) <> {} by A2;

then A6: dom f = A by FUNCT_2:def 1;

then reconsider fy = f . y as Function of B,C by A2, A4, A5, FUNCT_2:5, FUNCT_2:66;

A7: C <> {} by A1, A2, A4;

g . y in B by A1, A2, A4, A6, FUNCT_2:5;

then fy . (g . y) in C by A7, FUNCT_2:5;

hence x in C by A2, A3, PRALG_1:def 19; :: thesis: verum