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:14; :: thesis: verum