let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies |.(Base_FinSeq n,i).| = 1 )
assume ( 1 <= i & i <= n ) ; :: thesis: |.(Base_FinSeq n,i).| = 1
then sqrt (Sum (Base_FinSeq n,i)) = 1 by Th31, SQUARE_1:83;
hence |.(Base_FinSeq n,i).| = 1 by Th30; :: thesis: verum