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

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