let f, g be Function; :: thesis: rng <:f,g:> c= [:(rng f),(rng g):]
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in rng <:f,g:> or q in [:(rng f),(rng g):] )
assume q in rng <:f,g:> ; :: thesis: q in [:(rng f),(rng g):]
then consider x being set such that
A1: x in dom <:f,g:> and
A2: q = <:f,g:> . x by FUNCT_1:def 5;
x in (dom f) /\ (dom g) by A1, Def8;
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then ( f . x in rng f & g . x in rng g & q = [(f . x),(g . x)] ) by A1, A2, Def8, FUNCT_1:def 5;
hence q in [:(rng f),(rng g):] by ZFMISC_1:106; :: thesis: verum