let n be Nat; :: thesis: Pitag_dist n is_metric_of REAL n
let x, y, z be Element of REAL n; :: according to PCOMPS_1:def 7 :: thesis: ( ( not (Pitag_dist n) . x,y = 0 or x = y ) & ( not x = y or (Pitag_dist n) . x,y = 0 ) & (Pitag_dist n) . x,y = (Pitag_dist n) . y,x & (Pitag_dist n) . x,z <= ((Pitag_dist n) . x,y) + ((Pitag_dist n) . y,z) )
thus ( (Pitag_dist n) . x,y = 0 iff x = y ) :: thesis: ( (Pitag_dist n) . x,y = (Pitag_dist n) . y,x & (Pitag_dist n) . x,z <= ((Pitag_dist n) . x,y) + ((Pitag_dist n) . y,z) )

proof

(Pitag_dist n) . x,y = |.(x - y).| by Def6;
hence ( (Pitag_dist n) . x,y = 0 iff x = y ) by Th19; :: thesis: verum

end;

thus (Pitag_dist n) . x,y = |.(x - y).| by Def6
.= |.(y - x).| by Th21
.= (Pitag_dist n) . y,x by Def6 ; :: thesis: (Pitag_dist n) . x,z <= ((Pitag_dist n) . x,y) + ((Pitag_dist n) . y,z)
thus (Pitag_dist n) . x,z <= ((Pitag_dist n) . x,y) + ((Pitag_dist n) . y,z) :: thesis: verum

proof

( (Pitag_dist n) . x,y = |.(x - y).| & (Pitag_dist n) . x,z = |.(x - z).| & (Pitag_dist n) . y,z = |.(y - z).| ) by Def6;
hence (Pitag_dist n) . x,z <= ((Pitag_dist n) . x,y) + ((Pitag_dist n) . y,z) by Th22; :: thesis: verum

end;