let G be Group; :: thesis: for f being FinSequence of G holds Product (((Rev f) " ) ^ f) = 1_ G
let f be FinSequence of G; :: thesis: Product (((Rev f) " ) ^ f) = 1_ G
A1: len f = len (Rev f) by FINSEQ_5:def 3;
A2: len (Rev f) = len ((Rev f) " ) by Def4;
then A3: dom (Rev f) = dom ((Rev f) " ) by FINSEQ_3:31;
A4: len ((Rev f) " ) = len (Rev ((Rev f) " )) by FINSEQ_5:def 3;
A5: len (Rev ((Rev f) " )) = len ((Rev ((Rev f) " )) " ) by Def4;
then A6: dom (Rev ((Rev f) " )) = dom ((Rev ((Rev f) " )) " ) by FINSEQ_3:31;
for i being Nat st 1 <= i & i <= len f holds
f . i = ((Rev ((Rev f) " )) " ) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies f . i = ((Rev ((Rev f) " )) " ) . i )
A7: i in NAT by ORDINAL1:def 13;
assume A8: ( 1 <= i & i <= len f ) ; :: thesis: f . i = ((Rev ((Rev f) " )) " ) . i
then A9: i in Seg (len f) by A7;
then A10: i in dom f by FINSEQ_1:def 3;
A11: i in dom ((Rev ((Rev f) " )) " ) by A1, A2, A4, A5, A9, FINSEQ_1:def 3;
A12: (len f) - i = (len f) -' i by A8, XREAL_1:235;
((len f) - i) + 1 = ((len f) -' i) + 1 by A8, XREAL_1:235;
then reconsider j = ((len f) - i) + 1 as Element of NAT ;
A13: ((len f) - i) + 1 >= 0 + 1 by A12, XREAL_1:8;
i - 1 >= 0 by A8, XREAL_1:50;
then (len f) + 0 <= (len f) + (i - 1) by XREAL_1:9;
then (len f) - (i - 1) <= ((len f) + (i - 1)) - (i - 1) by XREAL_1:15;
then j in Seg (len f) by A13;
then A14: j in dom ((Rev f) " ) by A1, A2, FINSEQ_1:def 3;
A15: i + j = (len f) + 1 ;
A16: j + i = (len f) + 1 ;
f . i = f /. i by A10, PARTFUN1:def 8
.= (Rev f) /. j by A10, A15, FINSEQ_5:69
.= (((Rev f) /. j) " ) "
.= (((Rev f) " ) /. j) " by A3, A14, Def4
.= ((Rev ((Rev f) " )) /. i) " by A1, A2, A14, A16, FINSEQ_5:69
.= ((Rev ((Rev f) " )) " ) /. i by A6, A11, Def4
.= ((Rev ((Rev f) " )) " ) . i by A11, PARTFUN1:def 8 ;
hence f . i = ((Rev ((Rev f) " )) " ) . i ; :: thesis: verum

end;

then (Rev ((Rev f) " )) " = f by A1, A2, A4, A5, FINSEQ_1:18;
hence Product (((Rev f) " ) ^ f) = 1_ G by Th24; :: thesis: verum