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,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) )
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,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) )
( f is_a_pseudometric_of X iff ( f is Reflexive & f is symmetric & f is triangle ) ) by Def10;
hence ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) ) by METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5; :: thesis: verum