theorem Th11: :: TOPREALC:11

for n being Nat
for r, s being Real holds |.((n |-> r) - (n |-> s)).| = (sqrt n) * |.(r - s).|