reconsider MM = MetrStruct(# the carrier of M, the distance of M #) as MetrSpace by Lm1;

take MM ; :: thesis: ( the carrier of MM c= the carrier of M & ( for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y) ) )

thus the carrier of MM c= the carrier of M ; :: 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) = the distance of M . (x,y) ; :: thesis: verum

take MM ; :: thesis: ( the carrier of MM c= the carrier of M & ( for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y) ) )

thus the carrier of MM c= the carrier of M ; :: 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) = the distance of M . (x,y) ; :: thesis: verum