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