let F be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of F
for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
let V be VectSp of F; :: thesis: for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
let W be Subspace of V; :: thesis: for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
let f be linear-Functional of V; :: thesis: ( the carrier of W c= ker f implies QFunctional (f,W) is homogeneous )
set qf = QFunctional (f,W);
set vq = VectQuot (V,W);
assume A1: the carrier of W c= ker f ; :: thesis: QFunctional (f,W) is homogeneous

now :: thesis: for A being Vector of (VectQuot (V,W))
for r being Scalar of holds (QFunctional (f,W)) . (r * A) = r * ((QFunctional (f,W)) . A)

set C = CosetSet (V,W);
let A be Vector of (VectQuot (V,W)); :: thesis: for r being Scalar of holds (QFunctional (f,W)) . (r * A) = r * ((QFunctional (f,W)) . A)
let r be Scalar of ; :: thesis: (QFunctional (f,W)) . (r * A) = r * ((QFunctional (f,W)) . A)
A2: CosetSet (V,W) = the carrier of (VectQuot (V,W)) by Def6;
then A in CosetSet (V,W) ;
then consider aa being Coset of W such that
A3: A = aa ;
consider a being Vector of V such that
A4: aa = a + W by VECTSP_4:def 6;
r * A = the lmult of (VectQuot (V,W)) . (r,A)
.= (lmultCoset (V,W)) . (r,A) by Def6
.= (r * a) + W by A2, A3, A4, Def5 ;
hence (QFunctional (f,W)) . (r * A) = f . (r * a) by A1, Def12
.= r * (f . a) by HAHNBAN1:def 8
.= r * ((QFunctional (f,W)) . A) by A1, A3, A4, Def12 ;
:: thesis: verum

end;

hence QFunctional (f,W) is homogeneous ; :: thesis: verum