let z be FinSequence of COMPLEX ; :: thesis: (z *' ) *' = z
A1: len ((z *' ) *' ) = len (z *' ) by Def1;
A2: len (z *' ) = len z by Def1;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len ((z *' ) *' ) implies ((z *' ) *' ) . i = z . i )
assume ( 1 <= i & i <= len ((z *' ) *' ) ) ; :: thesis: ((z *' ) *' ) . i = z . i
then A3: ( 1 <= i & i <= len (z *' ) ) by Def1;
then (z *' ) . i = (z . i) *' by A2, Def1;
hence ((z *' ) *' ) . i = ((z . i) *' ) *' by A3, Def1
.= z . i ;
:: thesis: verum

end;

hence (z *' ) *' = z by A1, A2, FINSEQ_1:18; :: thesis: verum