let a be Real; :: thesis: for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)
let x be FinSequence of REAL ; :: thesis: ( len x > 0 implies ColVec2Mx (a * x) = a * (ColVec2Mx x) )
assume A1: len x > 0 ; :: thesis: ColVec2Mx (a * x) = a * (ColVec2Mx x)
A2: len (a * (ColVec2Mx x)) = len (ColVec2Mx x) by Th27
.= len x by A1, Def9 ;
A3: len (a * x) = len x by RVSUM_1:117;
then A4: dom (a * x) = dom x by FINSEQ_3:29;
A5: for j being Nat st j in dom (a * x) holds
(a * (ColVec2Mx x)) . j = <*((a * x) . j)*>

proof

len (ColVec2Mx x) = len x by A1, Def9;
then A6: dom (ColVec2Mx x) = dom x by FINSEQ_3:29;
let j be Nat; :: thesis: ( j in dom (a * x) implies (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> )
consider n being Nat such that
A7: for x2 being object st x2 in rng (a * (ColVec2Mx x)) holds
ex s2 being FinSequence st
( s2 = x2 & len s2 = n ) by MATRIX_0:def 1;
assume A8: j in dom (a * x) ; :: thesis: (a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
then A9: (ColVec2Mx x) . j = <*(x . j)*> by A1, A4, Def9;
A10: j in dom (a * (ColVec2Mx x)) by A2, A3, A8, FINSEQ_3:29;
then (a * (ColVec2Mx x)) . j in rng (a * (ColVec2Mx x)) by FUNCT_1:def 3;
then reconsider q = (a * (ColVec2Mx x)) . j as FinSequence of REAL by FINSEQ_1:def 11;
q in rng (a * (ColVec2Mx x)) by A10, FUNCT_1:def 3;
then A11: ex s2 being FinSequence st
( s2 = q & len s2 = n ) by A7;
consider s being FinSequence such that
A12: s in rng (a * (ColVec2Mx x)) and
A13: len s = width (a * (ColVec2Mx x)) by A1, A2, MATRIX_0:def 3;
ex s3 being FinSequence st
( s3 = s & len s3 = n ) by A12, A7;
then A14: len q = width (ColVec2Mx x) by A13, A11, Th27
.= 1 by A1, Def9
.= len <*((a * x) . j)*> by FINSEQ_1:40 ;
width (ColVec2Mx x) = 1 by A1, Def9;
then A15: 1 in Seg (width (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:1;
j in dom x by A3, A8, FINSEQ_3:29;
then A16: [j,1] in Indices (MXR2MXF (ColVec2Mx x)) by A6, A15, ZFMISC_1:87;
then A17: ex p3 being FinSequence of REAL st
( p3 = (ColVec2Mx x) . j & (ColVec2Mx x) * (j,1) = p3 . 1 ) by MATRIX_0:def 5;
[j,1] in Indices (a * (ColVec2Mx x)) by A16, Th28;
then A18: ex p being FinSequence of REAL st
( p = (a * (ColVec2Mx x)) . j & (a * (ColVec2Mx x)) * (j,1) = p . 1 ) by MATRIX_0:def 5;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A19: q . 1 = a * ((ColVec2Mx x) * (j,1)) by A16, A18, Th29
.= a * (x . j) by A17, A9
.= (a * x) . j by RVSUM_1:44
.= <*((a * x) . j)*> . 1 ;
for i being Nat st 1 <= i & i <= len <*((a * x) . j)*> holds
q . i = <*((a * x) . j)*> . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len <*((a * x) . j)*> implies q . i = <*((a * x) . j)*> . i )
A20: len <*((a * x) . j)*> = 1 by FINSEQ_1:40;
assume ( 1 <= i & i <= len <*((a * x) . j)*> ) ; :: thesis: q . i = <*((a * x) . j)*> . i
then i = 1 by A20, XXREAL_0:1;
hence q . i = <*((a * x) . j)*> . i by A19; :: thesis: verum

end;

hence (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> by A14, FINSEQ_1:14; :: thesis: verum

end;

width (a * (ColVec2Mx x)) = width (ColVec2Mx x) by Th27
.= 1 by A1, Def9 ;
hence ColVec2Mx (a * x) = a * (ColVec2Mx x) by A1, A2, A3, A5, Def9; :: thesis: verum