let f, g be Function; :: thesis: rng <:f,g:> c= [:(rng f),(rng g):]
let q be object ; :: 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 object such that
A1: x in dom <:f,g:> and
A2: q = <:f,g:> . x by FUNCT_1:def 3;
A3: x in (dom f) /\ (dom g) by A1, Def7;
then x in dom f by XBOOLE_0:def 4;
then A4: f . x in rng f by FUNCT_1:def 3;
x in dom g by A3, XBOOLE_0:def 4;
then A5: g . x in rng g by FUNCT_1:def 3;
q = [(f . x),(g . x)] by A1, A2, Def7;
hence q in [:(rng f),(rng g):] by A4, A5, ZFMISC_1:87; :: thesis: verum