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) = {{} }
consider a being Element of A;
A1: Funcs {} ,C = {{} } by FUNCT_5:64;
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 5;
f . y in rng f by A3, A6, FUNCT_1:def 5;
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 . a = {} by A1, TARSKI:def 1;
then (f .. g) . a = {} . (g . a) by A2, PRALG_1:def 17
.= {} by Th7 ;
then {} in rng (f .. g) by A3, A2, FUNCT_1:def 5;
hence rng (f .. g) = {{} } by A4, ZFMISC_1:39; :: thesis: verum