let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I st I is trivial holds
for p being non empty FinSequence of FreeAtoms G ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I st I is trivial holds
for p being non empty FinSequence of FreeAtoms G ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>
let G be Group-like multMagma-Family of I; :: thesis: ( I is trivial implies for p being non empty FinSequence of FreeAtoms G ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*> )
assume A1: I is trivial ; :: thesis: for p being non empty FinSequence of FreeAtoms G ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>
defpred S₁[ Nat] means for p being non empty FinSequence of FreeAtoms G st len p = $1 + 1 holds
ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>;
A2: S₁[ 0 ]

proof

let p be non empty FinSequence of FreeAtoms G; :: thesis: ( len p = 0 + 1 implies ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*> )
assume A3: len p = 0 + 1 ; :: thesis: ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>
then A4: p = <*(p . 1)*> by FINSEQ_1:40;
1 in dom p by A3, FINSEQ_3:25;
then A5: p . 1 in FreeAtoms G by FINSEQ_2:11;
then consider x, y being object such that
A6: p . 1 = [x,y] by RELAT_1:def 1;
x in dom G by A5, A6, Th7;
then A7: x = i by A1, ZFMISC_1:def 10;
then reconsider g = y as Element of (G . i) by A5, A6, Th9;
take g ; :: thesis: ReductionRel G reduces p,<*[i,g]*>
thus ReductionRel G reduces p,<*[i,g]*> by A4, A6, A7, REWRITE1:12; :: thesis: verum

end;

A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
let p be non empty FinSequence of FreeAtoms G; :: thesis: ( len p = (k + 1) + 1 implies ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*> )
assume A10: len p = (k + 1) + 1 ; :: thesis: ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>
len p <> 0 ;
then consider q being FinSequence of FreeAtoms G, d being Element of FreeAtoms G such that
A11: p = q ^ <*d*> by FINSEQ_2:19;
len p = (len q) + 1 by A11, FINSEQ_2:16;
then A12: len q = k + 1 by A10;
then not q is empty ;
then consider h being Element of (G . i) such that
A13: ReductionRel G reduces q,<*[i,h]*> by A9, A12;
consider x, y being object such that
A14: d = [x,y] by RELAT_1:def 1;
x in dom G by A14, Th7;
then A15: x = i by A1, ZFMISC_1:def 10;
then reconsider g = y as Element of (G . i) by A14, Th9;
A16: ( <*[i,g]*> is FinSequence of FreeAtoms G & <*[i,h]*> is FinSequence of FreeAtoms G ) by Th23;
ReductionRel G reduces <*d*>,<*[i,g]*> by A14, A15, REWRITE1:12;
then ReductionRel G reduces q ^ <*d*>,<*[i,h]*> ^ <*[i,g]*> by A13, A16, Th41;
then A17: ReductionRel G reduces p,<*[i,h],[i,g]*> by A11, FINSEQ_1:def 9;
take h * g ; :: thesis: ReductionRel G reduces p,<*[i,(h * g)]*>
[<*[i,h],[i,g]*>,<*[i,(h * g)]*>] in ReductionRel G by Th27;
then ReductionRel G reduces <*[i,h],[i,g]*>,<*[i,(h * g)]*> by REWRITE1:15;
hence ReductionRel G reduces p,<*[i,(h * g)]*> by A17, REWRITE1:16; :: thesis: verum

end;

A18: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A8);
let p be non empty FinSequence of FreeAtoms G; :: thesis: ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>
0 + 1 < (len p) + 1 by XREAL_1:8;
then 1 <= len p by NAT_1:13;
then consider k being Nat such that
A19: len p = 1 + k by NAT_1:10;
thus ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*> by A18, A19; :: thesis: verum