set q = quasinorm f;
thus quasinorm f is subadditive :: thesis: quasinorm f is homogeneous

proof

let v, w be Vector of V; :: according to HAHNBAN1:def 16 :: thesis: (quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w)
set fvw = signnorm f,(v + w);
set fv = signnorm f,v;
set fw = signnorm f,w;
A2: (quasinorm f) . v = sqrt (signnorm f,v) by Def10;
0 <= Re (f . v,v) by Def7;
then A3: 0 <= (quasinorm f) . v by A2, SQUARE_1:def 4;
A4: (quasinorm f) . w = sqrt (signnorm f,w) by Def10;
0 <= Re (f . w,w) by Def7;
then A5: 0 <= (quasinorm f) . w by A4, SQUARE_1:def 4;
( 0 <= Re (f . (v + w),(v + w)) & (quasinorm f) . (v + w) = sqrt (signnorm f,(v + w)) ) by Def7, Def10;
then (quasinorm f) . (v + w) <= sqrt ((((quasinorm f) . v) + ((quasinorm f) . w)) ^2 ) by A2, A4, Th50, SQUARE_1:94;
hence (quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w) by A3, A5, SQUARE_1:89; :: thesis: verum

end;

let v be Vector of V; :: according to HAHNBAN1:def 19 :: thesis: for b₁ being Element of the carrier of F_Complex holds (quasinorm f) . (b₁ * v) = |.b₁.| * ((quasinorm f) . v)
let r be Scalar of ; :: thesis: (quasinorm f) . (r * v) = |.r.| * ((quasinorm f) . v)
A6: ( 0 <= |.r.| ^2 & 0 <= Re (f . v,v) ) by Def7, XREAL_1:65;
A7: f . (r * v),(r * v) = r * (f . v,(r * v)) by BILINEAR:32
.= r * ((r *' ) * (f . v,v)) by Th30
.= (r * (r *' )) * (f . v,v)
.= [**(|.r.| ^2 ),0 **] * (f . v,v) by Th16
.= [**(|.r.| ^2 ),0 **] * [**(Re (f . v,v)),(Im (f . v,v))**] by COMPLEX1:29
.= [**(|.r.| ^2 ),0 **] * [**(Re (f . v,v)),0 **] by Def6
.= [**((|.r.| ^2 ) * (Re (f . v,v))),0 **] ;
thus (quasinorm f) . (r * v) = sqrt (signnorm f,(r * v)) by Def10
.= sqrt ((|.r.| ^2 ) * (Re (f . v,v))) by A7, COMPLEX1:28
.= (sqrt (|.r.| ^2 )) * (sqrt (Re (f . v,v))) by A6, SQUARE_1:97
.= |.r.| * (sqrt (signnorm f,v)) by COMPLEX1:132, SQUARE_1:89
.= |.r.| * ((quasinorm f) . v) by Def10 ; :: thesis: verum