let n be Nat; :: thesis: for r, s being Real holds |.((n |-> r) - (n |-> s)).| = (sqrt n) * |.(r - s).|
let r, s be Real; :: thesis: |.((n |-> r) - (n |-> s)).| = (sqrt n) * |.(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) * |.(r - s).| by COMPLEX1:72 ; :: thesis: verum