let f, g, h, k be Function; [:f,h:] * [:g,k:] = [:(f * g),(h * k):]
A1:
for x, y being object st x in dom (f * g) & y in dom (h * k) holds
([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y)
proof
let x,
y be
object ;
( x in dom (f * g) & y in dom (h * k) implies ([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y) )
assume that A2:
x in dom (f * g)
and A3:
y in dom (h * k)
;
([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y)
A4:
(
g . x in dom f &
k . y in dom h )
by A2, A3, FUNCT_1:11;
A5:
(
x in dom g &
y in dom k )
by A2, A3, FUNCT_1:11;
then
[x,y] in [:(dom g),(dom k):]
by ZFMISC_1:87;
then
[x,y] in dom [:g,k:]
by Def8;
hence ([:f,h:] * [:g,k:]) . (
x,
y) =
[:f,h:] . ([:g,k:] . (x,y))
by FUNCT_1:13
.=
[:f,h:] . (
(g . x),
(k . y))
by A5, Def8
.=
[(f . (g . x)),(h . (k . y))]
by A4, Def8
.=
[((f * g) . x),(h . (k . y))]
by A2, FUNCT_1:12
.=
[((f * g) . x),((h * k) . y)]
by A3, FUNCT_1:12
.=
[:(f * g),(h * k):] . (
x,
y)
by A2, A3, Def8
;
verum
end;
for p being object holds
( p in dom ([:f,h:] * [:g,k:]) iff p in [:(dom (f * g)),(dom (h * k)):] )
proof
let p be
object ;
( p in dom ([:f,h:] * [:g,k:]) iff p in [:(dom (f * g)),(dom (h * k)):] )
A6:
dom [:g,k:] = [:(dom g),(dom k):]
by Def8;
A7:
dom [:f,h:] = [:(dom f),(dom h):]
by Def8;
thus
(
p in dom ([:f,h:] * [:g,k:]) implies
p in [:(dom (f * g)),(dom (h * k)):] )
( p in [:(dom (f * g)),(dom (h * k)):] implies p in dom ([:f,h:] * [:g,k:]) )proof
assume A8:
p in dom ([:f,h:] * [:g,k:])
;
p in [:(dom (f * g)),(dom (h * k)):]
then A9:
[:g,k:] . p in dom [:f,h:]
by FUNCT_1:11;
A10:
p in dom [:g,k:]
by A8, FUNCT_1:11;
then consider x1,
x2 being
object such that A11:
x1 in dom g
and A12:
x2 in dom k
and A13:
p = [x1,x2]
by A6, ZFMISC_1:def 2;
[:g,k:] . (
x1,
x2)
= [:g,k:] . p
by A13;
then A14:
[(g . x1),(k . x2)] in dom [:f,h:]
by A6, A10, A9, A13, Th65;
then
k . x2 in dom h
by A7, ZFMISC_1:87;
then A15:
x2 in dom (h * k)
by A12, FUNCT_1:11;
g . x1 in dom f
by A7, A14, ZFMISC_1:87;
then
x1 in dom (f * g)
by A11, FUNCT_1:11;
hence
p in [:(dom (f * g)),(dom (h * k)):]
by A13, A15, ZFMISC_1:87;
verum
end;
assume
p in [:(dom (f * g)),(dom (h * k)):]
;
p in dom ([:f,h:] * [:g,k:])
then consider x1,
x2 being
object such that A16:
(
x1 in dom (f * g) &
x2 in dom (h * k) )
and A17:
p = [x1,x2]
by ZFMISC_1:def 2;
(
x1 in dom g &
x2 in dom k )
by A16, FUNCT_1:11;
then A18:
[x1,x2] in dom [:g,k:]
by A6, ZFMISC_1:87;
(
g . x1 in dom f &
k . x2 in dom h )
by A16, FUNCT_1:11;
then
[(g . x1),(k . x2)] in dom [:f,h:]
by A7, ZFMISC_1:87;
then
[:g,k:] . (
x1,
x2)
in dom [:f,h:]
by A6, A18, Th65;
hence
p in dom ([:f,h:] * [:g,k:])
by A17, A18, FUNCT_1:11;
verum
end;
then A19:
dom ([:f,h:] * [:g,k:]) = [:(dom (f * g)),(dom (h * k)):]
by TARSKI:2;
[:(dom (f * g)),(dom (h * k)):] = dom [:(f * g),(h * k):]
by Def8;
hence
[:f,h:] * [:g,k:] = [:(f * g),(h * k):]
by A19, A1, Th6; verum