theorem Th14: :: COUSIN:18

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