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:51
.= sqrt (Sum (n |-> ((r - s) ^2 ))) by RVSUM_1:82
.= sqrt (n * ((r - s) ^2 )) by RVSUM_1:110
.= (sqrt n) * (sqrt ((r - s) ^2 )) by SQUARE_1:97
.= (sqrt n) * (abs (r - s)) by COMPLEX1:158 ; :: thesis: verum