let X, Y, Z be set ; :: thesis: 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; :: thesis: for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:]
let g be Function of X,Z; :: thesis: rng <:f,g:> c= [:Y,Z:]
( rng f c= Y & rng g c= Z ) by RELAT_1:def 19;
then ( [:(rng f),(rng g):] c= [:Y,Z:] & rng <:f,g:> c= [:(rng f),(rng g):] ) by Th71, ZFMISC_1:119;
hence rng <:f,g:> c= [:Y,Z:] by XBOOLE_1:1; :: thesis: verum