let X, Y, Z be set ; for f being Function of X,Y
for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:]
let f be Function of X,Y; for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:]
let g be Function of X,Z; rng <:f,g:> c= [:Y,Z:]
( rng f c= Y & rng g c= Z )
by RELAT_1:def 19;
then A1:
[:(rng f),(rng g):] c= [:Y,Z:]
by ZFMISC_1:96;
rng <:f,g:> c= [:(rng f),(rng g):]
by Th51;
hence
rng <:f,g:> c= [:Y,Z:]
by A1; verum