let X be set ; :: thesis: for f being Function of [:X,X:],REAL holds

( f is_a_pseudometric_of X iff for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )

let f be Function of [:X,X:],REAL; :: thesis: ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )

thus ( f is_a_pseudometric_of X implies for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) :: thesis: ( ( for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X )

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X ) :: thesis: verum

( f is_a_pseudometric_of X iff for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )

let f be Function of [:X,X:],REAL; :: thesis: ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )

thus ( f is_a_pseudometric_of X implies for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) :: thesis: ( ( for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X )

proof

thus
( ( for a, b, c being Element of X holds
assume A1:
f is_a_pseudometric_of X
; :: thesis: for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) )

let a, b, c be Element of X; :: thesis: ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) )

f . (a,c) <= (f . (a,b)) + (f . (b,c)) by A1, Lm8;

hence ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) by A1, Lm8; :: thesis: verum

end;( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) )

let a, b, c be Element of X; :: thesis: ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) )

f . (a,c) <= (f . (a,b)) + (f . (b,c)) by A1, Lm8;

hence ( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) by A1, Lm8; :: thesis: verum

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X ) :: thesis: verum

proof

assume A2:
for a, b, c being Element of X holds

( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ; :: thesis: f is_a_pseudometric_of X

A3: for a, b being Element of X holds f . (a,b) = f . (b,a)

hence f is_a_pseudometric_of X ; :: thesis: verum

end;( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ; :: thesis: f is_a_pseudometric_of X

A3: for a, b being Element of X holds f . (a,b) = f . (b,a)

proof

for a, b, c being Element of X holds f . (a,c) <= (f . (a,b)) + (f . (b,c))
let a, b be Element of X; :: thesis: f . (a,b) = f . (b,a)

A4: ( f . (b,a) <= (f . (b,b)) + (f . (a,b)) & f . (b,b) = 0 ) by A2;

( f . (a,b) <= (f . (a,a)) + (f . (b,a)) & f . (a,a) = 0 ) by A2;

hence f . (a,b) = f . (b,a) by A4, XXREAL_0:1; :: thesis: verum

end;A4: ( f . (b,a) <= (f . (b,b)) + (f . (a,b)) & f . (b,b) = 0 ) by A2;

( f . (a,b) <= (f . (a,a)) + (f . (b,a)) & f . (a,a) = 0 ) by A2;

hence f . (a,b) = f . (b,a) by A4, XXREAL_0:1; :: thesis: verum

proof

then
( f is Reflexive & f is symmetric & f is triangle )
by A2, A3, METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5;
let x, y, z be Element of X; :: thesis: f . (x,z) <= (f . (x,y)) + (f . (y,z))

f . (x,z) <= (f . (x,y)) + (f . (z,y)) by A2;

hence f . (x,z) <= (f . (x,y)) + (f . (y,z)) by A3; :: thesis: verum

end;f . (x,z) <= (f . (x,y)) + (f . (z,y)) by A2;

hence f . (x,z) <= (f . (x,y)) + (f . (y,z)) by A3; :: thesis: verum

hence f is_a_pseudometric_of X ; :: thesis: verum