reconsider B = A as non empty set ;
set d = the distance of M || A;
A1: dom ( the distance of M || A) = (dom the distance of M) /\ [:A,A:] by RELAT_1:61
.= [: the carrier of M, the carrier of M:] /\ [:A,A:] by FUNCT_2:def 1
.= [:( the carrier of M /\ A),( the carrier of M /\ A):] by ZFMISC_1:100
.= [:( the carrier of M /\ A),A:] by XBOOLE_1:28
.= [:A,A:] by XBOOLE_1:28 ;
the distance of M || A = the distance of M | [:A,A:] ;
then rng ( the distance of M || A) c= REAL by RELAT_1:def 19;
then reconsider d = the distance of M || A as Function of [:B,B:],REAL by A1, FUNCT_2:def 1, RELSET_1:4;
set MM = MetrStruct(# B,d #);
A2: now :: thesis: for a, b being Element of MetrStruct(# B,d #) holds dist (a,b) = the distance of M . (a,b)
let a, b be Element of MetrStruct(# B,d #); :: thesis: dist (a,b) = the distance of M . (a,b)
thus dist (a,b) = the distance of MetrStruct(# B,d #) . (a,b)
.= the distance of M . [a,b] by A1, FUNCT_1:47
.= the distance of M . (a,b) ; :: thesis: verum
end;
now :: thesis: for a, b, c being Element of MetrStruct(# B,d #) holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
let a, b, c be Element of MetrStruct(# B,d #); :: thesis: ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
reconsider a9 = a, b9 = b, c9 = c as Point of M by TARSKI:def 3;
A3: dist (a,c) = the distance of M . (a,c) by A2
.= dist (a9,c9) ;
dist (a,b) = the distance of M . (a,b) by A2
.= dist (a9,b9) ;
hence ( dist (a,b) = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; :: thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A4: dist (b,c) = the distance of M . (b,c) by A2
.= dist (b9,c9) ;
thus dist (a,b) = the distance of M . (a9,b9) by A2
.= dist (b9,a9) by METRIC_1:def 1
.= the distance of M . (b9,a9)
.= dist (b,a) by A2 ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
dist (a,b) = the distance of M . (a,b) by A2
.= dist (a9,b9) ;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A4, METRIC_1:4; :: thesis: verum
end;
then reconsider MM = MetrStruct(# B,d #) as MetrSpace by METRIC_1:6;
now :: thesis: for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y)
let x, y be Point of MM; :: thesis: the distance of MM . (x,y) = the distance of M . (x,y)
thus the distance of MM . (x,y) = dist (x,y)
.= the distance of M . (x,y) by A2 ; :: thesis: verum
end;
then reconsider MM = MM as strict SubSpace of M by Def1;
take MM ; :: thesis: the carrier of MM = A
thus the carrier of MM = A ; :: thesis: verum