theorem Th28: :: MFOLD_2:28

for n being Nat holds Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*>