:: deftheorem Def1 defines *' COMPLSP2:def 1 :
for z, b₂ being FinSequence of COMPLEX holds
( b₂ = z *' iff ( len b₂ = len z & ( for i being Nat st 1 <= i & i <= len z holds
b₂ . i = (z . i) *' ) ) );