A1:
the carrier of (product G) = product (carr G)
by Th10;
ex x, y being set st
( x in product (carr G) & y in product (carr G) & not x = y )
proof
assume A2:
for
x,
y being
set st
x in product (carr G) &
y in product (carr G) holds
x = y
;
contradiction
consider z being
object such that A3:
z in product (carr G)
by XBOOLE_0:def 1;
consider g being
Function such that A4:
(
z = g &
dom g = dom (carr G) & ( for
i being
object st
i in dom (carr G) holds
g . i in (carr G) . i ) )
by A3, CARD_3:def 5;
set i = the
Element of
dom G;
now for r, s being object st r in the carrier of (G . the Element of dom G) & s in the carrier of (G . the Element of dom G) holds
r = slet r,
s be
object ;
( r in the carrier of (G . the Element of dom G) & s in the carrier of (G . the Element of dom G) implies r = s )assume A5:
(
r in the
carrier of
(G . the Element of dom G) &
s in the
carrier of
(G . the Element of dom G) )
;
r = s
(
g +* ( the
Element of
dom G,
r)
in the
carrier of
(product G) &
g +* ( the
Element of
dom G,
s)
in the
carrier of
(product G) )
by Th11, A3, A4, A5;
then
(
g +* ( the
Element of
dom G,
r)
in product (carr G) &
g +* ( the
Element of
dom G,
s)
in product (carr G) )
by Th10;
then A6:
g +* ( the
Element of
dom G,
r)
= g +* ( the
Element of
dom G,
s)
by A2;
the
Element of
dom G in dom G
;
then A7:
the
Element of
dom G in dom g
by A4, Lm1;
then
(g +* ( the Element of dom G,r)) . the
Element of
dom G = r
by FUNCT_7:31;
hence
r = s
by A6, A7, FUNCT_7:31;
verum end;
hence
contradiction
by ZFMISC_1:def 10;
verum
end;
hence
not product G is trivial
by A1; verum