let n be Nat; :: thesis: |.(0* n).| = 0
thus |.(0* n).| = sqrt (Sum (n |-> (0 ^2))) by RVSUM_1:82
.= sqrt (n * 0) by RVSUM_1:110
.= 0 by SQUARE_1:82 ; :: thesis: verum