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

proof

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

end;

assume q in [:(rng f),(rng g):] ; :: thesis: q in rng [:f,g:]
then consider y1, y2 being set such that
A6: y1 in rng f and
A7: y2 in rng g and
A8: q = [y1,y2] by ZFMISC_1:def 2;
consider x1 being set such that
A9: x1 in dom f and
A10: y1 = f . x1 by A6, FUNCT_1:def 5;
consider x2 being set such that
A11: x2 in dom g and
A12: y2 = g . x2 by A7, FUNCT_1:def 5;
( [x1,x2] in [:(dom f),(dom g):] & [:f,g:] . x1,x2 = q & dom [:f,g:] = [:(dom f),(dom g):] ) by A8, A9, A10, A11, A12, Def9, ZFMISC_1:106;
hence q in rng [:f,g:] by FUNCT_1:def 5; :: thesis: verum

end;

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