set lf = LQForm f;
thus
LQForm f is additiveFAF
:: thesis: LQForm f is cmplxhomogeneousFAF proof
let A be
Vector of
(VectQuot V,(LKer f));
:: according to BILINEAR:def 12 :: thesis: FunctionalFAF (LQForm f),A is additive
set flf =
FunctionalFAF (LQForm f),
A;
consider v being
Vector of
V such that A1:
A = v + (LKer f)
by VECTSP10:23;
let w,
t be
Vector of
W;
:: according to HAHNBAN1:def 11 :: thesis: (FunctionalFAF (LQForm f),A) . (w + t) = ((FunctionalFAF (LQForm f),A) . w) + ((FunctionalFAF (LQForm f),A) . t)
thus (FunctionalFAF (LQForm f),A) . (w + t) =
(LQForm f) . A,
(w + t)
by BILINEAR:9
.=
f . v,
(w + t)
by A1, BILINEAR:def 21
.=
(f . v,w) + (f . v,t)
by BILINEAR:28
.=
((LQForm f) . A,w) + (f . v,t)
by A1, BILINEAR:def 21
.=
((LQForm f) . A,w) + ((LQForm f) . A,t)
by A1, BILINEAR:def 21
.=
((FunctionalFAF (LQForm f),A) . w) + ((LQForm f) . A,t)
by BILINEAR:9
.=
((FunctionalFAF (LQForm f),A) . w) + ((FunctionalFAF (LQForm f),A) . t)
by BILINEAR:9
;
:: thesis: verum
end;
let A be Vector of (VectQuot V,(LKer f)); :: according to HERMITAN:def 4 :: thesis: FunctionalFAF (LQForm f),A is cmplxhomogeneous
set flf = FunctionalFAF (LQForm f),A;
consider v being Vector of V such that
A2:
A = v + (LKer f)
by VECTSP10:23;
let w be Vector of W; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (FunctionalFAF (LQForm f),A) . (a * w) = (a *' ) * ((FunctionalFAF (LQForm f),A) . w)
let r be Scalar of ; :: thesis: (FunctionalFAF (LQForm f),A) . (r * w) = (r *' ) * ((FunctionalFAF (LQForm f),A) . w)
thus (FunctionalFAF (LQForm f),A) . (r * w) =
(LQForm f) . A,(r * w)
by BILINEAR:9
.=
f . v,(r * w)
by A2, BILINEAR:def 21
.=
(r *' ) * (f . v,w)
by Th30
.=
(r *' ) * ((LQForm f) . A,w)
by A2, BILINEAR:def 21
.=
(r *' ) * ((FunctionalFAF (LQForm f),A) . w)
by BILINEAR:9
; :: thesis: verum