let f, g be Function; :: thesis: rng [:f,g:] = [:(rng f),(rng g):]
for q being object holds
( q in rng [:f,g:] iff q in [:(rng f),(rng g):] )

proof

let q be object ; :: thesis: ( q in rng [:f,g:] iff q in [:(rng f),(rng g):] )
A1: dom [:f,g:] = [:(dom f),(dom g):] by Def8;
thus ( q in rng [:f,g:] implies q in [:(rng f),(rng g):] ) :: thesis: ( q in [:(rng f),(rng g):] implies q in rng [:f,g:] )

proof

assume q in rng [:f,g:] ; :: thesis: q in [:(rng f),(rng g):]
then consider p being object such that
A2: p in dom [:f,g:] and
A3: q = [:f,g:] . p by FUNCT_1:def 3;
p in [:(dom f),(dom g):] by A2, Def8;
then consider x, y being object such that
A4: ( x in dom f & y in dom g ) and
A5: p = [x,y] by ZFMISC_1:def 2;
A6: ( f . x in rng f & g . y in rng g ) by A4, FUNCT_1:def 3;
q = [:f,g:] . (x,y) by A3, A5
.= [(f . x),(g . y)] by A4, Def8 ;
hence q in [:(rng f),(rng g):] by A6, ZFMISC_1:87; :: thesis: verum

end;

assume q in [:(rng f),(rng g):] ; :: thesis: q in rng [:f,g:]
then consider y1, y2 being object such that
A7: y1 in rng f and
A8: y2 in rng g and
A9: q = [y1,y2] by ZFMISC_1:def 2;
consider x2 being object such that
A10: x2 in dom g and
A11: y2 = g . x2 by A8, FUNCT_1:def 3;
consider x1 being object such that
A12: x1 in dom f and
A13: y1 = f . x1 by A7, FUNCT_1:def 3;
A14: [x1,x2] in [:(dom f),(dom g):] by A12, A10, ZFMISC_1:87;
[:f,g:] . (x1,x2) = q by A9, A12, A13, A10, A11, Def8;
hence q in rng [:f,g:] by A14, A1, FUNCT_1:def 3; :: thesis: verum

end;

hence rng [:f,g:] = [:(rng f),(rng g):] by TARSKI:2; :: thesis: verum