set M = MetrStruct(# {{} ,{{} }},Set_to_zero #);
MetrStruct(# {{} ,{{} }},Set_to_zero #) is PseudoMetricSpace

proof

A1: now

let x be Element of MetrStruct(# {{} ,{{} }},Set_to_zero #); :: thesis: dist x,x = 0
dist x,x = Set_to_zero . x,x by METRIC_1:def 1;
hence dist x,x = 0 by Th40; :: thesis: verum

end;

now

let x, y, z be Element of MetrStruct(# {{} ,{{} }},Set_to_zero #); :: thesis: ( dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) )
set x' = x;
set y' = y;
set z' = z;
A2: dist x,y = Set_to_zero . x,y by METRIC_1:def 1;
A3: dist y,x = Set_to_zero . y,x by METRIC_1:def 1;
A4: dist x,z = Set_to_zero . x,z by METRIC_1:def 1;
A5: dist y,z = Set_to_zero . y,z by METRIC_1:def 1;
thus dist x,y = dist y,x by A2, A3, Th42; :: thesis: dist x,z <= (dist x,y) + (dist y,z)
thus dist x,z <= (dist x,y) + (dist y,z) by A2, A4, A5, Th43; :: thesis: verum

end;

hence MetrStruct(# {{} ,{{} }},Set_to_zero #) is PseudoMetricSpace by A1, METRIC_1:1, METRIC_1:3, METRIC_1:4; :: thesis: verum

end;

hence ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) ; :: thesis: verum