:: deftheorem Def3 defines ProdFinSeq MEASUR13:def 3 :
for m being non zero Nat
for X, b₃ being b₁ -element FinSequence holds
( b₃ = ProdFinSeq X iff ( b₃ . 1 = X . 1 & ( for i being non zero Nat st i < m holds
b₃ . (i + 1) = [:(b₃ . i),(X . (i + 1)):] ) ) );