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:46;
0 <= Re (x .|. x) by Def11;
then A2: 0 <= |.(x .|. x).| by Th29;
||.(a * x).|| = sqrt |.(a * (x .|. (a * x))).| by Def11
.= sqrt |.(a * ((a *') * (x .|. x))).| by Th13
.= sqrt |.((a * (a *')) * (x .|. x)).|
.= sqrt (|.(a * (a *')).| * |.(x .|. x).|) by COMPLEX1:65
.= sqrt (|.(a * a).| * |.(x .|. x).|) by COMPLEX1:69
.= (sqrt |.(a * a).|) * (sqrt |.(x .|. x).|) by A1, A2, SQUARE_1:29
.= (sqrt (|.a.| ^2)) * (sqrt |.(x .|. x).|) by COMPLEX1:65
.= |.a.| * (sqrt |.(x .|. x).|) by COMPLEX1:46, SQUARE_1:22 ;
hence ||.(a * x).|| = |.a.| * ||.x.|| ; :: thesis: verum