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;
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 len g = 0 ;
then A1: 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 A1, FINSEQ_1:47;
hence Product (g ^ ((Rev g) " )) = 1_ G by GROUP_4:11; :: thesis: verum

end;

then A2: S₁[ 0 ] ;
A3: 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 A4: 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 A5: len g <= k + 1 ; :: thesis: Product (g ^ ((Rev g) " )) = 1_ G

now

per cases ( len g < k + 1 or len g = k + 1 ) by A5, 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 A4; :: thesis: verum

end;

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

then A7: k < len g by NAT_1:13;
reconsider h = g | k as FinSequence of G ;
A8: len h = k by A7, FINSEQ_1:80;
A9: g = h ^ <*(g /. (k + 1))*> by A6, 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 A10: g ^ ((Rev g) " ) = h ^ (<*(g /. (k + 1))*> ^ ((<*(g /. (k + 1))*> " ) ^ ((Rev h) " ))) by A9, FINSEQ_1:45
.= h ^ ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> " )) ^ ((Rev h) " )) by FINSEQ_1:45 ;
A11: 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 ;
Product (g ^ ((Rev g) " )) = (Product h) * (Product ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> " )) ^ ((Rev h) " ))) by A10, 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 A11, GROUP_1:def 5
.= Product (h ^ ((Rev h) " )) by GROUP_4:8 ;
hence Product (g ^ ((Rev g) " )) = 1_ G by A4, A8; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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