for K being Field
for m, i being Element of NAT st 1 <= i & i <= m holds
|((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K