set lf = RQForm f;
thus
RQForm f is additiveSAF
:: thesis: RQForm f is homogeneousSAF proof
let A be
Vector of
(VectQuot W,(RKer f));
:: according to BILINEAR:def 13 :: thesis: FunctionalSAF (RQForm f),A is additive
set flf =
FunctionalSAF (RQForm f),
A;
consider w being
Vector of
W such that A3:
A = w + (RKer f)
by VECTSP10:23;
let v,
t be
Vector of
V;
:: according to HAHNBAN1:def 11 :: thesis: (FunctionalSAF (RQForm f),A) . (v + t) = ((FunctionalSAF (RQForm f),A) . v) + ((FunctionalSAF (RQForm f),A) . t)
thus (FunctionalSAF (RQForm f),A) . (v + t) =
(RQForm f) . (v + t),
A
by Th10
.=
f . (v + t),
w
by A3, Def22
.=
(f . v,w) + (f . t,w)
by Th27
.=
((RQForm f) . v,A) + (f . t,w)
by A3, Def22
.=
((RQForm f) . v,A) + ((RQForm f) . t,A)
by A3, Def22
.=
((FunctionalSAF (RQForm f),A) . v) + ((RQForm f) . t,A)
by Th10
.=
((FunctionalSAF (RQForm f),A) . v) + ((FunctionalSAF (RQForm f),A) . t)
by Th10
;
:: thesis: verum
end;
let A be Vector of (VectQuot W,(RKer f)); :: according to BILINEAR:def 15 :: thesis: FunctionalSAF (RQForm f),A is homogeneous
set flf = FunctionalSAF (RQForm f),A;
consider w being Vector of W such that
A4:
A = w + (RKer f)
by VECTSP10:23;
let v be Vector of V; :: according to HAHNBAN1:def 12 :: thesis: for b1 being Element of the carrier of K holds (FunctionalSAF (RQForm f),A) . (b1 * v) = b1 * ((FunctionalSAF (RQForm f),A) . v)
let r be Scalar of ; :: thesis: (FunctionalSAF (RQForm f),A) . (r * v) = r * ((FunctionalSAF (RQForm f),A) . v)
thus (FunctionalSAF (RQForm f),A) . (r * v) =
(RQForm f) . (r * v),A
by Th10
.=
f . (r * v),w
by A4, Def22
.=
r * (f . v,w)
by Th32
.=
r * ((RQForm f) . v,A)
by A4, Def22
.=
r * ((FunctionalSAF (RQForm f),A) . v)
by Th10
; :: thesis: verum