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, Th29, SQUARE_1:83;
hence |.(Base_FinSeq n,i).| = 1 by Th28; :: thesis: verum