set p = ProductMap ((Carrier F),(Carrier G),h);
A3:
[#] (product F) = product (Carrier F)
by GROUP_7:def 2;
reconsider p = ProductMap ((Carrier F),(Carrier G),h) as Function of (product F),(product G) by A3, GROUP_7:def 2;
for a, b being Element of (product F) holds p . (a * b) = (p . a) * (p . b)
proof
let a,
b be
Element of
(product F);
p . (a * b) = (p . a) * (p . b)
A5:
dom (p . (a * b)) = I
by Th3;
A6:
dom ((p . a) * (p . b)) = I
by Th3;
for
i being
object st
i in I holds
(p . (a * b)) . i = ((p . a) * (p . b)) . i
proof
let i be
object ;
( i in I implies (p . (a * b)) . i = ((p . a) * (p . b)) . i )
assume
i in I
;
(p . (a * b)) . i = ((p . a) * (p . b)) . i
then reconsider i =
i as
Element of
I ;
consider hi being
Homomorphism of
(F . i),
(G . i) such that A8:
(
hi = h . i &
(p . (a * b)) . i = hi . ((a * b) . i) )
by A1, Th38;
consider hi1 being
Homomorphism of
(F . i),
(G . i) such that A9:
(
hi1 = h . i &
(p . a) . i = hi1 . (a . i) )
by A1, Th38;
consider hi2 being
Homomorphism of
(F . i),
(G . i) such that A10:
(
hi2 = h . i &
(p . b) . i = hi2 . (b . i) )
by A1, Th38;
a in product F
;
then
a . i in F . i
by Th5;
then reconsider ai =
a . i as
Element of
(F . i) ;
b in product F
;
then
b . i in F . i
by Th5;
then reconsider bi =
b . i as
Element of
(F . i) ;
(p . (a * b)) . i =
hi . (ai * bi)
by A8, GROUP_7:1
.=
(hi . ai) * (hi . bi)
by GROUP_6:def 6
.=
((p . a) * (p . b)) . i
by A8, A9, A10, GROUP_7:1
;
hence
(p . (a * b)) . i = ((p . a) * (p . b)) . i
;
verum
end;
hence
p . (a * b) = (p . a) * (p . b)
by A5, A6, FUNCT_1:2;
verum
end;
hence
ProductMap ((Carrier F),(Carrier G),h) is Homomorphism of (product F),(product G)
by GROUP_6:def 6; verum