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

proof

per cases ( B <> {} or B = {} ) ;

suppose B <> {} ; :: thesis: dom f = dom g

then C1: dom g = A by FUNCT_2:def 1;
Funcs (B,C) <> {} by a1, FUNCT_2:8;
hence dom f = dom g by C1, FUNCT_2:def 1; :: thesis: verum

end;

suppose B = {} ; :: thesis: dom f = dom g

hence dom f = dom g by A1; :: thesis: verum

end;

end;

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