let V be RealLinearSpace; :: thesis: for W being Subspace of V
for A being VECTOR of (VectQuot (V,W))
for v being VECTOR of V
for a being Real st A = v + W holds
a * A = (a * v) + W
let W be Subspace of V; :: thesis: for A being VECTOR of (VectQuot (V,W))
for v being VECTOR of V
for a being Real st A = v + W holds
a * A = (a * v) + W
set X = RLSp2RVSp V;
set Y = RLSp2RVSp W;
let A be VECTOR of (VectQuot (V,W)); :: thesis: for v being VECTOR of V
for a being Real st A = v + W holds
a * A = (a * v) + W
let v be VECTOR of V; :: thesis: for a being Real st A = v + W holds
a * A = (a * v) + W
let a be Real; :: thesis: ( A = v + W implies a * A = (a * v) + W )
assume A1: A = v + W ; :: thesis: a * A = (a * v) + W
reconsider v1 = v as Vector of (RLSp2RVSp V) ;
reconsider A1 = A as Vector of (VectQuot ((RLSp2RVSp V),(RLSp2RVSp W))) ;
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
A2: A1 = v1 + (RLSp2RVSp W) by A1, LMQ03;
thus a * A = a1 * A1
.= (a1 * v1) + (RLSp2RVSp W) by A2, VECTSP10:25
.= (a * v) + W by LMQ03 ; :: thesis: verum