let n be Element of NAT ; :: thesis: |.(1* n).| = sqrt n
reconsider f = n |-> (1 ^2 ) as FinSequence of REAL by FINSEQ_2:77;
thus |.(1* n).| = sqrt (Sum f) by RVSUM_1:82
.= sqrt (n * 1) by RVSUM_1:110
.= sqrt n ; :: thesis: verum