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) = {{} }
A1: Funcs {} ,C = {{} } by FUNCT_5:64;
A2: dom (f .. g) = dom f by PRALG_1:def 17;
A3: rng (f .. g) c= {{} }

proof

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

end;

consider a being Element of A;
A8: dom f = A by A1, FUNCT_2:def 1;
f . a = {} by A1, TARSKI:def 1;
then (f .. g) . a = {} . (g . a) by A8, PRALG_1:def 17
.= {} by Th7 ;
then {} in rng (f .. g) by A2, A8, FUNCT_1:def 5;
hence rng (f .. g) = {{} } by A3, ZFMISC_1:39; :: thesis: verum