let n be Nat; :: thesis: |.(1* n).| = sqrt n
reconsider j = 1 ^2 as Element of REAL by XREAL_0:def 1;
reconsider f = n |-> j as FinSequence of REAL ;
thus |.(1* n).| = sqrt (Sum f) by RVSUM_1:56
.= sqrt (n * 1) by RVSUM_1:80
.= sqrt n ; :: thesis: verum