let X be non empty compact TopSpace; :: thesis: for x being Point of
for y being Point of st x = y holds
||.x.|| = ||.y.||
let x be Point of ; :: thesis: for y being Point of st x = y holds
||.x.|| = ||.y.||
thus for y being Point of st x = y holds
||.x.|| = ||.y.|| by FUNCT_1:72; :: thesis: verum