let G be Group; :: thesis: for f being FinSequence of G holds Product (f ^ ((Rev f) ")) = 1_ G
let f be FinSequence of G; :: thesis: Product (f ^ ((Rev f) ")) = 1_ G
defpred S₁[ Nat] means for g being FinSequence of G st len g <= $1 holds
Product (g ^ ((Rev g) ")) = 1_ G;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
for g being FinSequence of G st len g <= k + 1 holds
Product (g ^ ((Rev g) ")) = 1_ G

proof

let g be FinSequence of G; :: thesis: ( len g <= k + 1 implies Product (g ^ ((Rev g) ")) = 1_ G )
assume A3: len g <= k + 1 ; :: thesis: Product (g ^ ((Rev g) ")) = 1_ G

now :: thesis: ( ( len g < k + 1 & Product (g ^ ((Rev g) ")) = 1_ G ) or ( len g = k + 1 & Product (g ^ ((Rev g) ")) = 1_ G ) )

per cases ( len g < k + 1 or len g = k + 1 ) by A3, XXREAL_0:1;

case len g < k + 1 ; :: thesis: Product (g ^ ((Rev g) ")) = 1_ G

then len g <= k by NAT_1:13;
hence Product (g ^ ((Rev g) ")) = 1_ G by A2; :: thesis: verum

end;

case A4: len g = k + 1 ; :: thesis: Product (g ^ ((Rev g) ")) = 1_ G

reconsider h = g | k as FinSequence of G ;
k < len g by A4, NAT_1:13;
then A5: len h = k by FINSEQ_1:59;
A6: Product (<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) = (Product <*(g /. (k + 1))*>) * (Product (<*(g /. (k + 1))*> ")) by GROUP_4:5
.= (g /. (k + 1)) * (Product (<*(g /. (k + 1))*> ")) by FINSOP_1:11
.= (g /. (k + 1)) * (Product <*((g /. (k + 1)) ")*>) by Th22
.= (g /. (k + 1)) * ((g /. (k + 1)) ") by FINSOP_1:11
.= 1_ G by GROUP_1:def 5 ;
A7: g = h ^ <*(g /. (k + 1))*> by A4, FINSEQ_5:21;
then Rev g = <*(g /. (k + 1))*> ^ (Rev h) by FINSEQ_5:63;
then (Rev g) " = (<*(g /. (k + 1))*> ") ^ ((Rev h) ") by Th21;
then g ^ ((Rev g) ") = h ^ (<*(g /. (k + 1))*> ^ ((<*(g /. (k + 1))*> ") ^ ((Rev h) "))) by A7, FINSEQ_1:32
.= h ^ ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) ^ ((Rev h) ")) by FINSEQ_1:32 ;
then Product (g ^ ((Rev g) ")) = (Product h) * (Product ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) ^ ((Rev h) "))) by GROUP_4:5
.= (Product h) * ((Product (<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> "))) * (Product ((Rev h) "))) by GROUP_4:5
.= (Product h) * (Product ((Rev h) ")) by A6, GROUP_1:def 4
.= Product (h ^ ((Rev h) ")) by GROUP_4:5 ;
hence Product (g ^ ((Rev g) ")) = 1_ G by A2, A5; :: thesis: verum

end;

end;

end;

hence Product (g ^ ((Rev g) ")) = 1_ G ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for g being FinSequence of G st len g <= 0 holds
Product (g ^ ((Rev g) ")) = 1_ G

proof

let g be FinSequence of G; :: thesis: ( len g <= 0 implies Product (g ^ ((Rev g) ")) = 1_ G )
assume len g <= 0 ; :: thesis: Product (g ^ ((Rev g) ")) = 1_ G
then A8: g = <*> the carrier of G ;
then Rev g = <*> the carrier of G by FINSEQ_5:79;
then (Rev g) " = <*> the carrier of G by Th20;
then g ^ ((Rev g) ") = <*> the carrier of G by A8, FINSEQ_1:34;
hence Product (g ^ ((Rev g) ")) = 1_ G by GROUP_4:8; :: thesis: verum

end;

then A9: S₁[ 0 ] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A9, A1);
then S₁[ len f] ;
hence Product (f ^ ((Rev f) ")) = 1_ G ; :: thesis: verum