let a be Complex; :: thesis: for X being ComplexUnitarySpace
for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||
let X be ComplexUnitarySpace; :: 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 * a).| by COMPLEX1:132;
0 <= Re (x .|. x) by Def13;
then A2: 0 <= |.(x .|. x).| by Th36;
||.(a * x).|| = sqrt |.(a * (x .|. (a * x))).| by Def13
.= sqrt |.(a * ((a *' ) * (x .|. x))).| by Th20
.= sqrt |.((a * (a *' )) * (x .|. x)).|
.= sqrt (|.(a * (a *' )).| * |.(x .|. x).|) by COMPLEX1:151
.= sqrt (|.(a * a).| * |.(x .|. x).|) by COMPLEX1:155
.= (sqrt |.(a * a).|) * (sqrt |.(x .|. x).|) by A1, A2, SQUARE_1:97
.= (sqrt (|.a.| ^2 )) * (sqrt |.(x .|. x).|) by COMPLEX1:151
.= |.a.| * (sqrt |.(x .|. x).|) by COMPLEX1:132, SQUARE_1:89 ;
hence ||.(a * x).|| = |.a.| * ||.x.|| ; :: thesis: verum