set lf = LQForm f;
thus
LQForm f is additiveFAF
LQForm f is homogeneousFAF proof
let A be
Vector of
(VectQuot V,(LKer f));
BILINEAR:def 12 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;
HAHNBAN1:def 11 (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 Th9
.=
f . v,
(w + t)
by A1, Def21
.=
(f . v,w) + (f . v,t)
by Th28
.=
((LQForm f) . A,w) + (f . v,t)
by A1, Def21
.=
((LQForm f) . A,w) + ((LQForm f) . A,t)
by A1, Def21
.=
((FunctionalFAF (LQForm f),A) . w) + ((LQForm f) . A,t)
by Th9
.=
((FunctionalFAF (LQForm f),A) . w) + ((FunctionalFAF (LQForm f),A) . t)
by Th9
;
verum
end;
let A be Vector of (VectQuot V,(LKer f)); BILINEAR:def 14 FunctionalFAF (LQForm f),A is homogeneous
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; HAHNBAN1:def 12 for b1 being Element of the carrier of K holds (FunctionalFAF (LQForm f),A) . (b1 * w) = b1 * ((FunctionalFAF (LQForm f),A) . w)
let r be Scalar of ; (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 Th9
.=
f . v,(r * w)
by A2, Def21
.=
r * (f . v,w)
by Th33
.=
r * ((LQForm f) . A,w)
by A2, Def21
.=
r * ((FunctionalFAF (LQForm f),A) . w)
by Th9
; verum