let f, g be Function; ( f is one-to-one & g is one-to-one implies [:f,g:] " = [:(f "),(g "):] )
assume that
A1:
f is one-to-one
and
A2:
g is one-to-one
; [:f,g:] " = [:(f "),(g "):]
A3:
[:f,g:] is one-to-one
by A1, A2;
A4:
dom (f ") = rng f
by A1, FUNCT_1:33;
A5:
dom (g ") = rng g
by A2, FUNCT_1:33;
A6: dom ([:f,g:] ") =
rng [:f,g:]
by A3, FUNCT_1:33
.=
[:(dom (f ")),(dom (g ")):]
by A4, A5, FUNCT_3:67
;
for x, y being object st x in dom (f ") & y in dom (g ") holds
([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)]
proof
let x,
y be
object ;
( x in dom (f ") & y in dom (g ") implies ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] )
assume that A7:
x in dom (f ")
and A8:
y in dom (g ")
;
([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)]
A9:
dom [:f,g:] = [:(dom f),(dom g):]
by FUNCT_3:def 8;
A10:
(f ") . x in rng (f ")
by A7, FUNCT_1:def 3;
A11:
(g ") . y in rng (g ")
by A8, FUNCT_1:def 3;
A12:
(f ") . x in dom f
by A1, A10, FUNCT_1:33;
(g ") . y in dom g
by A2, A11, FUNCT_1:33;
then A13:
[((f ") . x),((g ") . y)] in dom [:f,g:]
by A9, A12, ZFMISC_1:87;
A14:
f . ((f ") . x) =
(f * (f ")) . x
by A7, FUNCT_1:13
.=
(((f ") ") * (f ")) . x
by A1, FUNCT_1:43
.=
(id (dom (f "))) . x
by A1, FUNCT_1:39
.=
x
by A7, FUNCT_1:18
;
g . ((g ") . y) =
(g * (g ")) . y
by A8, FUNCT_1:13
.=
(((g ") ") * (g ")) . y
by A2, FUNCT_1:43
.=
(id (dom (g "))) . y
by A2, FUNCT_1:39
.=
y
by A8, FUNCT_1:18
;
then
[:f,g:] . (
((f ") . x),
((g ") . y))
= [x,y]
by A9, A13, A14, FUNCT_3:65;
hence
([:f,g:] ") . (
x,
y)
= [((f ") . x),((g ") . y)]
by A1, A2, A13, FUNCT_1:32;
verum
end;
hence
[:f,g:] " = [:(f "),(g "):]
by A6, FUNCT_3:def 8; verum