let I be non empty set ; for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H st len p = len q & ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) holds
( ReductionRel H reduces p ^ q, {} & ReductionRel H reduces q ^ p, {} )
let H be Group-like associative multMagma-Family of I; for p, q being FinSequence of FreeAtoms H st len p = len q & ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) holds
( ReductionRel H reduces p ^ q, {} & ReductionRel H reduces q ^ p, {} )
let p, q be FinSequence of FreeAtoms H; ( len p = len q & ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) implies ( ReductionRel H reduces p ^ q, {} & ReductionRel H reduces q ^ p, {} ) )
assume that
A1:
len p = len q
and
A2:
for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")]
; ( ReductionRel H reduces p ^ q, {} & ReductionRel H reduces q ^ p, {} )
for k being Nat
for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]
by A2, Lm1;
hence
ReductionRel H reduces p ^ q, {}
by A1, Th33; ReductionRel H reduces q ^ p, {}
for k being Nat
for i being Element of I
for h being Element of (H . i) st q . k = [i,h] holds
(Rev p) . k = [i,(h ")]
proof
let k be
Nat;
for i being Element of I
for h being Element of (H . i) st q . k = [i,h] holds
(Rev p) . k = [i,(h ")]let i be
Element of
I;
for h being Element of (H . i) st q . k = [i,h] holds
(Rev p) . k = [i,(h ")]let h be
Element of
(H . i);
( q . k = [i,h] implies (Rev p) . k = [i,(h ")] )
assume A3:
q . k = [i,h]
;
(Rev p) . k = [i,(h ")]
then A4:
k in dom q
by FUNCT_1:def 2;
then
k in Seg (len p)
by A1, FINSEQ_1:def 3;
then A5:
((len p) - k) + 1
in Seg (len p)
by FINSEQ_5:2;
then reconsider m =
((len p) - k) + 1 as
Nat ;
A6:
m in dom p
by A5, FINSEQ_1:def 3;
then
p . m in rng p
by FUNCT_1:3;
then A7:
p . m in FreeAtoms H
;
then consider i9,
g being
object such that A8:
p . m = [i9,g]
by RELAT_1:def 1;
i9 in dom H
by A7, A8, Th7;
then reconsider i9 =
i9 as
Element of
I ;
reconsider g =
g as
Element of
(H . i9) by A7, A8, Th9;
A9:
m in dom q
by A1, A6, FINSEQ_3:29;
[i9,(g ")] =
(Rev q) . m
by A2, A8
.=
q . (((len q) - m) + 1)
by A9, FINSEQ_5:58
.=
[i,h]
by A1, A3
;
then A10:
(
i9 = i &
g " = h )
by XTUPLE_0:1;
then reconsider g =
g as
Element of
(H . i) ;
dom p = dom q
by A1, FINSEQ_3:29;
hence
(Rev p) . k = [i,(h ")]
by A4, A8, A10, FINSEQ_5:58;
verum
end;
then
for k being Nat
for i being Element of I
for h, g being Element of (H . i) st q . k = [i,h] & h * g = 1_ (H . i) holds
(Rev p) . k = [i,g]
by Lm1;
hence
ReductionRel H reduces q ^ p, {}
by A1, Th33; verum