let f, g be Function; :: thesis: rng |:f,g:| c= [:(rng f),(rng g):]
let z be set ; :: 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 set such that
A1: p in dom |:f,g:| and
A2: z = |:f,g:| . p by FUNCT_1:def 5;
consider x, y, x', y' being set such that
A3: p = [[x,x'],[y,y']] and
A4: ( [x,y] in dom f & [x',y'] in dom g ) by A1, Def3;
A5: ( f . [x,y] in rng f & g . [x',y'] in rng g ) by A4, FUNCT_1:def 5;
z = |:f,g:| . [x,x'],[y,y'] by A2, A3
.= [(f . x,y),(g . x',y')] by A4, Def3 ;
hence z in [:(rng f),(rng g):] by A5, ZFMISC_1:106; :: thesis: verum