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) st g <> 1_ (G . i) holds
<*[i,g]*> is_a_normal_form_wrt ReductionRel G
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I
for g being Element of (G . i) st g <> 1_ (G . i) holds
<*[i,g]*> is_a_normal_form_wrt ReductionRel G
let G be Group-like multMagma-Family of I; :: thesis: for g being Element of (G . i) st g <> 1_ (G . i) holds
<*[i,g]*> is_a_normal_form_wrt ReductionRel G
let g be Element of (G . i); :: thesis: ( g <> 1_ (G . i) implies <*[i,g]*> is_a_normal_form_wrt ReductionRel G )
assume A1: g <> 1_ (G . i) ; :: thesis: <*[i,g]*> is_a_normal_form_wrt ReductionRel G

now :: thesis: for q being object holds not [<*[i,g]*>,q] in ReductionRel G

set p = <*[i,g]*>;
given q being object such that A2: [<*[i,g]*>,q] in ReductionRel G ; :: thesis: contradiction
( <*[i,g]*> in field (ReductionRel G) & q in field (ReductionRel G) ) by A2, RELAT_1:15;
then ( <*[i,g]*> in (FreeAtoms G) * & q in (FreeAtoms G) * ) by Th30;
then reconsider p = <*[i,g]*>, q = q as FinSequence of FreeAtoms G by FINSEQ_1:def 11;

per cases ( ex s, t being FinSequence of FreeAtoms G ex j being Element of I st
( p = (s ^ <*[j,(1_ (G . j))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex j being Element of I ex h1, h2 being Element of (G . j) st
( p = (s ^ <*[j,h1],[j,h2]*>) ^ t & q = (s ^ <*[j,(h1 * h2)]*>) ^ t ) ) by A2, Def3;

suppose ex s, t being FinSequence of FreeAtoms G ex j being Element of I st
( p = (s ^ <*[j,(1_ (G . j))]*>) ^ t & q = s ^ t ) ; :: thesis: contradiction

then consider s, t being FinSequence of FreeAtoms G, j being Element of I such that
A3: ( p = (s ^ <*[j,(1_ (G . j))]*>) ^ t & q = s ^ t ) ;
0 + 1 = len p by FINSEQ_1:40
.= (len (s ^ <*[j,(1_ (G . j))]*>)) + (len t) by A3, FINSEQ_1:22
.= ((len s) + 1) + (len t) by FINSEQ_2:16 ;
then (len s) + (len t) = 0 ;
then A4: ( s = {} & t = {} ) ;
then p = <*[j,(1_ (G . j))]*> ^ t by A3, FINSEQ_1:34
.= <*[j,(1_ (G . j))]*> by A4, FINSEQ_1:34 ;
then [i,g] = [j,(1_ (G . j))] by FINSEQ_1:76;
then ( i = j & g = 1_ (G . j) ) by XTUPLE_0:1;
hence contradiction by A1; :: thesis: verum

end;

suppose ex s, t being FinSequence of FreeAtoms G ex j being Element of I ex h1, h2 being Element of (G . j) st
( p = (s ^ <*[j,h1],[j,h2]*>) ^ t & q = (s ^ <*[j,(h1 * h2)]*>) ^ t ) ; :: thesis: contradiction

then consider s, t being FinSequence of FreeAtoms G, j being Element of I, h1, h2 being Element of (G . j) such that
A5: ( p = (s ^ <*[j,h1],[j,h2]*>) ^ t & q = (s ^ <*[j,(h1 * h2)]*>) ^ t ) ;
0 + 1 = len p by FINSEQ_1:40
.= (len (s ^ <*[j,h1],[j,h2]*>)) + (len t) by A5, FINSEQ_1:22
.= ((len s) + (len <*[j,h1],[j,h2]*>)) + (len t) by FINSEQ_1:22
.= ((len s) + 2) + (len t) by FINSEQ_1:44
.= (((len s) + (len t)) + 1) + 1 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence <*[i,g]*> is_a_normal_form_wrt ReductionRel G by REWRITE1:def 5; :: thesis: verum