let G be Group; for f being FinSequence of G holds Product (((Rev f) ") ^ f) = 1_ G
let f be FinSequence of G; Product (((Rev f) ") ^ f) = 1_ G
A1:
len f = len (Rev f)
by FINSEQ_5:def 3;
A2:
len (Rev ((Rev f) ")) = len ((Rev ((Rev f) ")) ")
by Def3;
then A3:
dom (Rev ((Rev f) ")) = dom ((Rev ((Rev f) ")) ")
by FINSEQ_3:29;
A4:
len ((Rev f) ") = len (Rev ((Rev f) "))
by FINSEQ_5:def 3;
A5:
len (Rev f) = len ((Rev f) ")
by Def3;
then A6:
dom (Rev f) = dom ((Rev f) ")
by FINSEQ_3:29;
for i being Nat st 1 <= i & i <= len f holds
f . i = ((Rev ((Rev f) ")) ") . i
proof
let i be
Nat;
( 1 <= i & i <= len f implies f . i = ((Rev ((Rev f) ")) ") . i )
assume that A7:
1
<= i
and A8:
i <= len f
;
f . i = ((Rev ((Rev f) ")) ") . i
((len f) - i) + 1
= ((len f) -' i) + 1
by A8, XREAL_1:233;
then reconsider j =
((len f) - i) + 1 as
Nat ;
A9:
i + j = (len f) + 1
;
A10:
i in Seg (len f)
by A7, A8;
then A11:
i in dom ((Rev ((Rev f) ")) ")
by A1, A5, A4, A2, FINSEQ_1:def 3;
i - 1
>= 0
by A7, XREAL_1:48;
then
(len f) + 0 <= (len f) + (i - 1)
by XREAL_1:7;
then A12:
(len f) - (i - 1) <= ((len f) + (i - 1)) - (i - 1)
by XREAL_1:13;
(len f) - i = (len f) -' i
by A8, XREAL_1:233;
then
((len f) - i) + 1
>= 0 + 1
by XREAL_1:6;
then
j in Seg (len f)
by A12;
then A13:
j in dom ((Rev f) ")
by A1, A5, FINSEQ_1:def 3;
A14:
j + i = (len f) + 1
;
A15:
i in dom f
by A10, FINSEQ_1:def 3;
then f . i =
f /. i
by PARTFUN1:def 6
.=
(Rev f) /. j
by A15, A9, FINSEQ_5:66
.=
(((Rev f) /. j) ") "
.=
(((Rev f) ") /. j) "
by A6, A13, Def3
.=
((Rev ((Rev f) ")) /. i) "
by A1, A5, A13, A14, FINSEQ_5:66
.=
((Rev ((Rev f) ")) ") /. i
by A3, A11, Def3
.=
((Rev ((Rev f) ")) ") . i
by A11, PARTFUN1:def 6
;
hence
f . i = ((Rev ((Rev f) ")) ") . i
;
verum
end;
then
(Rev ((Rev f) ")) " = f
by A1, A5, A4, A2;
hence
Product (((Rev f) ") ^ f) = 1_ G
by Th23; verum