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

A2: now

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

end;

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