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 11 :: 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);
A1: (quasinorm f) . v = sqrt (signnorm (f,v)) by Def10;
0 <= Re (f . (v,v)) by Def7;
then A2: 0 <= (quasinorm f) . v by A1, SQUARE_1:def 2;
A3: (quasinorm f) . w = sqrt (signnorm (f,w)) by Def10;
0 <= Re (f . (w,w)) by Def7;
then A4: 0 <= (quasinorm f) . w by A3, SQUARE_1:def 2;
( 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 A1, A3, Th47, SQUARE_1:26;
hence (quasinorm f) . (v + w) <= ((quasinorm f) . v) + ((quasinorm f) . w) by A2, A4, SQUARE_1:22; :: thesis: verum

end;

let v be Vector of V; :: according to HAHNBAN1:def 14 :: 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)
A5: ( 0 <= |.r.| ^2 & 0 <= Re (f . (v,v)) ) by Def7, XREAL_1:63;
A6: f . ((r * v),(r * v)) = r * (f . (v,(r * v))) by BILINEAR:31
.= r * ((r *') * (f . (v,v))) by Th27
.= (r * (r *')) * (f . (v,v))
.= [**(|.r.| ^2),0**] * (f . (v,v)) by Th13
.= [**(|.r.| ^2),0**] * [**(Re (f . (v,v))),(Im (f . (v,v)))**] by COMPLEX1:13
.= [**(|.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 A6, COMPLEX1:12
.= (sqrt (|.r.| ^2)) * (sqrt (Re (f . (v,v)))) by A5, SQUARE_1:29
.= |.r.| * (sqrt (signnorm (f,v))) by COMPLEX1:46, SQUARE_1:22
.= |.r.| * ((quasinorm f) . v) by Def10 ; :: thesis: verum