let F1, F2 be Function of (TopSpaceMetr M),R^1; :: thesis: ( ( for x being Point of M holds F1 . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds F2 . x = lower_bound ((dist x) .: P) ) implies F1 = F2 )

assume A10: for y being Point of M holds F1 . y = lower_bound ((dist y) .: P) ; :: thesis: ( ex x being Point of M st not F2 . x = lower_bound ((dist x) .: P) or F1 = F2 )

assume A11: for y being Point of M holds F2 . y = lower_bound ((dist y) .: P) ; :: thesis: F1 = F2

for y being object st y in the carrier of (TopSpaceMetr M) holds

F1 . y = F2 . y

assume A10: for y being Point of M holds F1 . y = lower_bound ((dist y) .: P) ; :: thesis: ( ex x being Point of M st not F2 . x = lower_bound ((dist x) .: P) or F1 = F2 )

assume A11: for y being Point of M holds F2 . y = lower_bound ((dist y) .: P) ; :: thesis: F1 = F2

for y being object st y in the carrier of (TopSpaceMetr M) holds

F1 . y = F2 . y

proof

hence
F1 = F2
by FUNCT_2:12; :: thesis: verum
let y be object ; :: thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y )

A12: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;

assume y in the carrier of (TopSpaceMetr M) ; :: thesis: F1 . y = F2 . y

then reconsider y = y as Point of M by A12;

F1 . y = lower_bound ((dist y) .: P) by A10

.= F2 . y by A11 ;

hence F1 . y = F2 . y ; :: thesis: verum

end;A12: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;

assume y in the carrier of (TopSpaceMetr M) ; :: thesis: F1 . y = F2 . y

then reconsider y = y as Point of M by A12;

F1 . y = lower_bound ((dist y) .: P) by A10

.= F2 . y by A11 ;

hence F1 . y = F2 . y ; :: thesis: verum