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) st g <> 1_ (H . i) holds
nf [*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) st g <> 1_ (H . i) holds
nf [*i,g*] = <*[i,g]*>
let H be Group-like associative multMagma-Family of I; :: thesis: for g being Element of (H . i) st g <> 1_ (H . i) holds
nf [*i,g*] = <*[i,g]*>
let g be Element of (H . i); :: thesis: ( g <> 1_ (H . i) implies nf [*i,g*] = <*[i,g]*> )
assume g <> 1_ (H . i) ; :: thesis: nf [*i,g*] = <*[i,g]*>
then A1: <*[i,g]*> is_a_normal_form_wrt ReductionRel H by Th38;
[i,g] in FreeAtoms H by Th9;
then <*[i,g]*> is FinSequence of FreeAtoms H by FINSEQ_1:74;
hence nf [*i,g*] = <*[i,g]*> by A1, Th48, Def7; :: thesis: verum