let a be Real; :: thesis: for X being RealUnitarySpace
for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||
let X be RealUnitarySpace; :: thesis: for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||
let x be Point of X; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||
A1: ( 0 <= a ^2 & 0 <= x .|. x ) by Def2, XREAL_1:63;
||.(a * x).|| = sqrt (a * (x .|. (a * x))) by Def2
.= sqrt (a * (a * (x .|. x))) by Def2
.= sqrt ((a ^2) * (x .|. x))
.= (sqrt (a ^2)) * (sqrt (x .|. x)) by A1, SQUARE_1:29
.= |.a.| * (sqrt (x .|. x)) by COMPLEX1:72 ;
hence ||.(a * x).|| = |.a.| * ||.x.|| ; :: thesis: verum