let G be Group; :: thesis: for a being Element of G holds <*a*> " = <*(a ")*>
let a be Element of G; :: thesis: <*a*> " = <*(a ")*>
A1: len (<*a*> ") = len <*a*> by Def4
.= 1 by FINSEQ_1:39
.= len <*(a ")*> by FINSEQ_1:39 ;
for i being Nat st 1 <= i & i <= len <*(a ")*> holds
(<*a*> ") . i = <*(a ")*> . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len <*(a ")*> implies (<*a*> ") . i = <*(a ")*> . i )
assume A2: ( 1 <= i & i <= len <*(a ")*> ) ; :: thesis: (<*a*> ") . i = <*(a ")*> . i
A3: len <*(a ")*> = 1 by FINSEQ_1:39;
then A4: i = 1 by A2, XXREAL_0:1;
A5: i in NAT by ORDINAL1:def 12;
len <*a*> = 1 by FINSEQ_1:39;
then i in Seg (len <*a*>) by A2, A5, A3;
then A6: i in dom <*a*> by FINSEQ_1:def 3;
i in Seg (len (<*a*> ")) by A1, A2, A5;
then i in dom (<*a*> ") by FINSEQ_1:def 3;
then A7: (<*a*> ") . i = (<*a*> ") /. i by PARTFUN1:def 6
.= (<*a*> /. i) " by A6, Def4 ;
<*a*> /. i = <*a*> . i by A6, PARTFUN1:def 6
.= a by A4, FINSEQ_1:40 ;
hence (<*a*> ") . i = <*(a ")*> . i by A4, A7, FINSEQ_1:40; :: thesis: verum

end;

hence <*a*> " = <*(a ")*> by A1, FINSEQ_1:14; :: thesis: verum