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.|

||.((a ") * x).|| = |.(a ").| * ||.x.|| by NORMSP_1:def 1;

hence ||.((a ") * x).|| = ||.x.|| / |.a.| by COMPLEX1:66; :: 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.|

||.((a ") * x).|| = |.(a ").| * ||.x.|| by NORMSP_1:def 1;

hence ||.((a ") * x).|| = ||.x.|| / |.a.| by COMPLEX1:66; :: thesis: verum