theorem Th29: :: EUCLID_7:30

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