let f, g be Function; 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 ;
( 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):] )
( q in [:(rng f),(rng g):] implies q in rng [:f,g:] )proof
assume
q in rng [:f,g:]
;
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;
verum
end;
assume
q in [:(rng f),(rng g):]
;
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;
verum
end;
hence
rng [:f,g:] = [:(rng f),(rng g):]
by TARSKI:2; verum