let I be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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)

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; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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)

proof

hence
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
by A4, A5, Th1; :: thesis: verum
let j be Element of I; :: thesis: ( i <> j implies (g1 * g2) . j = 1_ (F . j) )

assume A6: i <> j ; :: thesis: (g1 * g2) . j = 1_ (F . j)

then A7: g1 . j = 1_ (F . j) by Th1, A1;

g2 . j = 1_ (F . j) by A6, Th1, A1;

hence (g1 * g2) . j = (1_ (F . j)) * (1_ (F . j)) by A7, GROUP_7:1

.= 1_ (F . j) by GROUP_1:def 4 ;

:: thesis: verum

end;assume A6: i <> j ; :: thesis: (g1 * g2) . j = 1_ (F . j)

then A7: g1 . j = 1_ (F . j) by Th1, A1;

g2 . j = 1_ (F . j) by A6, Th1, A1;

hence (g1 * g2) . j = (1_ (F . j)) * (1_ (F . j)) by A7, GROUP_7:1

.= 1_ (F . j) by GROUP_1:def 4 ;

:: thesis: verum