let n be Element of NAT ; :: thesis: |.(1* n).| = sqrt n
reconsider f = n |-> (1 ^2) 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