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