let A be non empty set ; :: thesis: for G being Function of [:A,A:],REAL st G is_metric_of A holds
bounded_metric A,G is_metric_of A
let G be Function of [:A,A:],REAL ; :: thesis: ( G is_metric_of A implies bounded_metric A,G is_metric_of A )
assume A1: G is_metric_of A ; :: thesis: bounded_metric A,G is_metric_of A
A2: for a, b, c being Element of A holds (bounded_metric A,G) . a,c <= ((bounded_metric A,G) . a,b) + ((bounded_metric A,G) . b,c)

proof

let a, b, c be Element of A; :: thesis: (bounded_metric A,G) . a,c <= ((bounded_metric A,G) . a,b) + ((bounded_metric A,G) . b,c)
set a1 = G . a,b;
set a3 = G . a,c;
set a5 = G . b,c;
A3: ( (bounded_metric A,G) . a,b = (G . a,b) / (1 + (G . a,b)) & (bounded_metric A,G) . a,c = (G . a,c) / (1 + (G . a,c)) ) by Def4;
A4: (bounded_metric A,G) . b,c = (G . b,c) / (1 + (G . b,c)) by Def4;
A5: G . a,c >= 0 by A1, Th2;
A6: ( 0 <= G . a,b & 0 <= G . b,c ) by A1, Th2;
then A7: 0 <> (1 + (G . a,b)) * (1 + (G . b,c)) by XCMPLX_1:6;
A8: ((G . a,b) / (1 + (G . a,b))) + ((G . b,c) / (1 + (G . b,c))) = (((G . a,b) * (1 + (G . b,c))) + ((G . b,c) * (1 + (G . a,b)))) / ((1 + (G . a,b)) * (1 + (G . b,c))) by A6, XCMPLX_1:117
.= ((((G . a,b) * 1) + ((G . a,b) * (G . b,c))) + (((G . b,c) * 1) + ((G . b,c) * (G . a,b)))) / ((1 + (G . a,b)) * (1 + (G . b,c))) ;
0 <= G . a,c by A1, Th2;
then A9: (((G . a,b) / (1 + (G . a,b))) + ((G . b,c) / (1 + (G . b,c)))) - ((G . a,c) / (1 + (G . a,c))) = (((((G . a,b) + ((G . a,b) * (G . b,c))) + ((G . b,c) + ((G . b,c) * (G . a,b)))) * (1 + (G . a,c))) - ((G . a,c) * ((1 + (G . a,b)) * (1 + (G . b,c))))) / (((1 + (G . a,b)) * (1 + (G . b,c))) * (1 + (G . a,c))) by A7, A8, XCMPLX_1:131;
A10: ( G . a,b >= 0 & G . b,c >= 0 ) by A1, Th2;
G . a,c <= (G . a,b) + (G . b,c) by A1, PCOMPS_1:def 7;
then ((G . a,b) + (G . b,c)) - (G . a,c) >= 0 by XREAL_1:50;
then (((G . b,c) + (G . a,b)) - (G . a,c)) + (((G . a,b) * (G . b,c)) + (((G . b,c) * (G . a,b)) + (((G . b,c) * (G . a,b)) * (G . a,c)))) >= 0 by A10, A5;
hence (bounded_metric A,G) . a,c <= ((bounded_metric A,G) . a,b) + ((bounded_metric A,G) . b,c) by A3, A4, A9, A10, A5, XREAL_1:51; :: thesis: verum

end;

A11: for a, b being Element of A holds
( (bounded_metric A,G) . a,b = 0 iff a = b )

proof

let a, b be Element of A; :: thesis: ( (bounded_metric A,G) . a,b = 0 iff a = b )
A12: ( (bounded_metric A,G) . a,b = 0 implies a = b )

proof

assume (bounded_metric A,G) . a,b = 0 ; :: thesis: a = b
then A13: (G . a,b) / (1 + (G . a,b)) = 0 by Def4;
0 <= G . a,b by A1, Th2;
then G . a,b = 0 by A13, XCMPLX_1:50;
hence a = b by A1, PCOMPS_1:def 7; :: thesis: verum

end;

( a = b implies (bounded_metric A,G) . a,b = 0 )

proof

assume a = b ; :: thesis: (bounded_metric A,G) . a,b = 0
then G . a,b = 0 by A1, PCOMPS_1:def 7;
then (G . a,b) / (1 + (G . a,b)) = 0 ;
hence (bounded_metric A,G) . a,b = 0 by Def4; :: thesis: verum

end;

hence ( (bounded_metric A,G) . a,b = 0 iff a = b ) by A12; :: thesis: verum

end;

for a, b being Element of A holds (bounded_metric A,G) . a,b = (bounded_metric A,G) . b,a

proof

let a, b be Element of A; :: thesis: (bounded_metric A,G) . a,b = (bounded_metric A,G) . b,a
(G . a,b) / (1 + (G . a,b)) = (G . b,a) / (1 + (G . a,b)) by A1, PCOMPS_1:def 7
.= (G . b,a) / (1 + (G . b,a)) by A1, PCOMPS_1:def 7
.= (bounded_metric A,G) . b,a by Def4 ;
hence (bounded_metric A,G) . a,b = (bounded_metric A,G) . b,a by Def4; :: thesis: verum

end;

hence bounded_metric A,G is_metric_of A by A11, A2, PCOMPS_1:def 7; :: thesis: verum