X1:
the carrier of (product G) = product (carr G)
by LM001;
ex x, y being set st
( x in product (carr G) & y in product (carr G) & not x = y )
proof
assume A0:
for
x,
y being
set st
x in product (carr G) &
y in product (carr G) holds
x = y
;
contradiction
consider z being
set such that P0:
z in product (carr G)
by XBOOLE_0:def 1;
consider g being
Function such that P1:
(
z = g &
dom g = dom (carr G) & ( for
i being
set st
i in dom (carr G) holds
g . i in (carr G) . i ) )
by P0, CARD_3:def 5;
set i = the
Element of
dom G;
now let r,
s be
set ;
( 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 P2:
(
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 LM003, P0, P1, P2;
then
(
g +* ( the
Element of
dom G,
r)
in product (carr G) &
g +* ( the
Element of
dom G,
s)
in product (carr G) )
by LM001;
then KK:
g +* ( the
Element of
dom G,
r)
= g +* ( the
Element of
dom G,
s)
by A0;
the
Element of
dom G in dom G
;
then F1:
the
Element of
dom G in dom g
by P1, ZE;
then
(g +* ( the Element of dom G,r)) . the
Element of
dom G = r
by FUNCT_7:31;
hence
r = s
by KK, F1, FUNCT_7:31;
verum end;
hence
contradiction
by ZFMISC_1:def 10;
verum
end;
hence
not product G is trivial
by X1, ZFMISC_1:def 10; verum