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₁[ Element of NAT ] means for g being FinSequence of G st len g <= $1 holds
Product (g ^ ((Rev g) ")) = 1_ G;
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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

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:80;
A6: Product (<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) = (Product <*(g /. (k + 1))*>) * (Product (<*(g /. (k + 1))*> ")) by GROUP_4:8
.= (g /. (k + 1)) * (Product (<*(g /. (k + 1))*> ")) by FINSOP_1:12
.= (g /. (k + 1)) * (Product <*((g /. (k + 1)) ")*>) by Th23
.= (g /. (k + 1)) * ((g /. (k + 1)) ") by FINSOP_1:12
.= 1_ G by GROUP_1:def 6 ;
A7: g = h ^ <*(g /. (k + 1))*> by A4, FINSEQ_5:24;
then Rev g = <*(g /. (k + 1))*> ^ (Rev h) by FINSEQ_5:66;
then (Rev g) " = (<*(g /. (k + 1))*> ") ^ ((Rev h) ") by Th22;
then g ^ ((Rev g) ") = h ^ (<*(g /. (k + 1))*> ^ ((<*(g /. (k + 1))*> ") ^ ((Rev h) "))) by A7, FINSEQ_1:45
.= h ^ ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) ^ ((Rev h) ")) by FINSEQ_1:45 ;
then Product (g ^ ((Rev g) ")) = (Product h) * (Product ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) ^ ((Rev h) "))) by GROUP_4:8
.= (Product h) * ((Product (<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> "))) * (Product ((Rev h) "))) by GROUP_4:8
.= (Product h) * (Product ((Rev h) ")) by A6, GROUP_1:def 5
.= Product (h ^ ((Rev h) ")) by GROUP_4:8 ;
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:82;
then (Rev g) " = <*> the carrier of G by Th21;
then g ^ ((Rev g) ") = <*> the carrier of G by A8, FINSEQ_1:47;
hence Product (g ^ ((Rev g) ")) = 1_ G by GROUP_4:11; :: thesis: verum

end;

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