let a be real number ; :: thesis: for X being RealNormSpace
for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a)
let X be RealNormSpace; :: thesis: for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a)
let x be Point of X; :: thesis: ||.((a ") * x).|| = ||.x.|| / (abs a)
thus ||.((a ") * x).|| = (abs (a ")) * ||.x.|| by NORMSP_1:def 1
.= ((abs a) ") * ||.x.|| by COMPLEX1:66
.= (1 / (abs a)) * ||.x.|| by XCMPLX_1:215
.= ||.x.|| / (abs a) by XCMPLX_1:99 ; :: thesis: verum