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 Def1;
A4: (bounded_metric (A,G)) . (b,c) = (G . (b,c)) / (1 + (G . (b,c))) by Def1;
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:116
.= ((((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:130;
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 6;
then ((G . (a,b)) + (G . (b,c))) - (G . (a,c)) >= 0 by XREAL_1:48;
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:49; :: 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 Def1;
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 6; :: 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 6;
then (G . (a,b)) / (1 + (G . (a,b))) = 0 ;
hence (bounded_metric (A,G)) . (a,b) = 0 by Def1; :: 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 6
.= (G . (b,a)) / (1 + (G . (b,a))) by A1, PCOMPS_1:def 6
.= (bounded_metric (A,G)) . (b,a) by Def1 ;
hence (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a) by Def1; :: thesis: verum

end;

hence bounded_metric (A,G) is_metric_of A by A11, A2, PCOMPS_1:def 6; :: thesis: verum