let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies |.(Base_FinSeq (n,i)).| = 1 )
assume that
A1: 1 <= i and
A2: i <= n ; :: thesis: |.(Base_FinSeq (n,i)).| = 1
sqrt (Sum (Base_FinSeq (n,i))) = 1 by A1, A2, Th26, SQUARE_1:18;
hence |.(Base_FinSeq (n,i)).| = 1 by Th25; :: thesis: verum