let C be set ; :: thesis: for A being non empty set
for f being Function of A,(Funcs ({},C))
for g being Function of A,{} holds rng (f .. g) = {{}}
let A be non empty set ; :: thesis: for f being Function of A,(Funcs ({},C))
for g being Function of A,{} holds rng (f .. g) = {{}}
let f be Function of A,(Funcs ({},C)); :: thesis: for g being Function of A,{} holds rng (f .. g) = {{}}
let g be Function of A,{}; :: thesis: rng (f .. g) = {{}}
set a = the Element of A;
A1: Funcs ({},C) = {{}} by FUNCT_5:57;
then A2: dom f = A by FUNCT_2:def 1;
A3: dom (f .. g) = dom f by PRALG_1:def 17;
A4: rng (f .. g) c= {{}}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f .. g) or x in {{}} )
A5: rng f c= Funcs ({},C) by RELAT_1:def 19;
assume x in rng (f .. g) ; :: thesis: x in {{}}
then consider y being set such that
A6: y in dom (f .. g) and
A7: (f .. g) . y = x by FUNCT_1:def 3;
f . y in rng f by A3, A6, FUNCT_1:def 3;
then A8: f . y = {} by A1, A5, TARSKI:def 1;
x = (f . y) . (g . y) by A3, A6, A7, PRALG_1:def 17;
then x = {} by A8, Th7;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

f . the Element of A = {} by A1, TARSKI:def 1;
then (f .. g) . the Element of A = {} . (g . the Element of A) by A2, PRALG_1:def 17
.= {} by Th7 ;
then {} in rng (f .. g) by A3, A2, FUNCT_1:def 3;
hence rng (f .. g) = {{}} by A4, ZFMISC_1:33; :: thesis: verum