let n be Element of NAT ; :: thesis: |.(0c n).| = 0
thus |.(0c n).| = sqrt (Sum (sqr (n |-> 0 ))) by Th60
.= sqrt (Sum (n |-> (0 ^2 ))) by RVSUM_1:82
.= sqrt (n * 0 ) by RVSUM_1:110
.= 0 by SQUARE_1:82 ; :: thesis: verum