let f, g be Function; :: thesis: rng |:f,g:| c= [:(rng f),(rng g):]
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng |:f,g:| or z in [:(rng f),(rng g):] )
assume z in rng |:f,g:| ; :: thesis: z in [:(rng f),(rng g):]
then consider p being object such that
A1: p in dom |:f,g:| and
A2: z = |:f,g:| . p by FUNCT_1:def 3;
consider x, y, x9, y9 being object such that
A3: p = [[x,x9],[y,y9]] and
A4: ( [x,y] in dom f & [x9,y9] in dom g ) by A1, Def3;
A5: ( f . [x,y] in rng f & g . [x9,y9] in rng g ) by A4, FUNCT_1:def 3;
z = |:f,g:| . ([x,x9],[y,y9]) by A2, A3
.= [(f . (x,y)),(g . (x9,y9))] by A4, Def3 ;
hence z in [:(rng f),(rng g):] by A5, ZFMISC_1:87; :: thesis: verum