let I be non empty set ; for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let F be Group-like associative multMagma-Family of I; for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let i be Element of I; for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let g1, g2 be Element of (product F); for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let z1, z2 be Element of (F . i); ( g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) implies g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) )
assume A1:
( g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) )
; g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
set x1 = g1;
set x2 = g2;
A2:
( g1 = g1 & dom g1 = I & g1 . i = z1 & ( for j being Element of I st j <> i holds
g1 . j = 1_ (F . j) ) )
by Th1, A1;
A3:
( g2 = g2 & dom g2 = I & g2 . i = z2 & ( for j being Element of I st j <> i holds
g2 . j = 1_ (F . j) ) )
by Th1, A1;
set x12 = g1 * g2;
the carrier of (product F) = product (Carrier F)
by GROUP_7:def 2;
then A4:
dom (g1 * g2) = I
by PARTFUN1:def 2;
A5:
(g1 * g2) . i = z1 * z2
by A2, A3, GROUP_7:1;
for j being Element of I st i <> j holds
(g1 * g2) . j = 1_ (F . j)
hence
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
by A4, A5, Th1; verum