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

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