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:56
.= len <*(a " )*> by FINSEQ_1:56 ;
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: i in NAT by ORDINAL1:def 13;
A4: len <*(a " )*> = 1 by FINSEQ_1:56;
then A5: i = 1 by A2, XXREAL_0:1;
len <*a*> = 1 by FINSEQ_1:56;
then i in Seg (len <*a*>) by A2, A3, A4;
then A6: i in dom <*a*> by FINSEQ_1:def 3;
i in Seg (len (<*a*> " )) by A1, A2, A3;
then i in dom (<*a*> " ) by FINSEQ_1:def 3;
then A7: (<*a*> " ) . i = (<*a*> " ) /. i by PARTFUN1:def 8
.= (<*a*> /. i) " by A6, Def4 ;
<*a*> /. i = <*a*> . i by A6, PARTFUN1:def 8
.= a by A5, FINSEQ_1:57 ;
hence (<*a*> " ) . i = <*(a " )*> . i by A5, A7, FINSEQ_1:57; :: thesis: verum

end;

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