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 )

proof

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;

thus ( ( 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 ) :: 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

proof

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;

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

proof

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;

then ( f is Reflexive & f is symmetric & f is triangle ) by A2, A3, METRIC_1:def 3, METRIC_1:def 5, METRIC_1:def 6;
hence f is_a_pseudometric_of X by Def10; :: thesis: verum

end;