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