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;
dom (f .. g) = (dom f) /\ (dom g) by PRALG_1:def 19
.= {} ;
hence rng (f .. g) = {} by RELAT_1:42; :: thesis: verum