theorem Th14: :: COUSIN:20

for n being Nat holds distance_by_norm_of (REAL-NS n) = Pitag_dist n