theorem Th27: :: EUCLID_7:28

for i, n being Nat st 1 <= i & i <= n holds
|.(Base_FinSeq (n,i)).| = 1