let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> = (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> = (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g
let G be Group-like multMagma-Family of I; :: thesis: for g being Element of (G . i) holds <*[i,g]*> = (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g
let g be Element of (G . i); :: thesis: <*[i,g]*> = (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g
set C = the carrier of (G . i);
A1: dom <:( the carrier of (G . i) --> i),(id the carrier of (G . i)):> = the carrier of (G . i) by Lm3;
thus (commute <*<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):>*>) . g = <*(<:( the carrier of (G . i) --> i),(id the carrier of (G . i)):> . g)*> by A1, Th4
.= <*[(( the carrier of (G . i) --> i) . g),((id the carrier of (G . i)) . g)]*> by A1, FUNCT_3:def 7
.= <*[i,g]*> ; :: thesis: verum