let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds [*i,g*] " = [*i,(g ")*]
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds [*i,g*] " = [*i,(g ")*]
let H be Group-like associative multMagma-Family of I; :: thesis: for g being Element of (H . i) holds [*i,g*] " = [*i,(g ")*]
let g be Element of (H . i); :: thesis: [*i,g*] " = [*i,(g ")*]
[*i,g*] * [*i,(g ")*] = [*i,(g * (g "))*] by Th51
.= [*i,(1_ (H . i))*] by GROUP_1:def 5
.= 1_ (FreeProduct H) by Th49 ;
hence [*i,g*] " = [*i,(g ")*] by GROUP_1:12; :: thesis: verum