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

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