let n be Nat; :: thesis: for r, s being real number holds |.((n |-> r) - (n |-> s)).| = (sqrt n) * (abs (r - s))
let r, s be real number ; :: thesis: |.((n |-> r) - (n |-> s)).| = (sqrt n) * (abs (r - s))
thus |.((n |-> r) - (n |-> s)).| = sqrt (Sum (sqr (n |-> (r - s)))) by RVSUM_1:30
.= sqrt (Sum (n |-> ((r - s) ^2))) by RVSUM_1:56
.= sqrt (n * ((r - s) ^2)) by RVSUM_1:80
.= (sqrt n) * (sqrt ((r - s) ^2)) by SQUARE_1:29
.= (sqrt n) * (abs (r - s)) by COMPLEX1:72 ; :: thesis: verum