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: width (a * (ColVec2Mx x)) = width (ColVec2Mx x) by Th27
.= 1 by A1, Def9 ;
A4: len (a * x) = len x by EUCLID_2:8;
then A5: dom (a * x) = dom x by FINSEQ_3:31;
for j being Nat st j in dom (a * x) holds
(a * (ColVec2Mx x)) . j = <*((a * x) . j)*>

proof

let j be Nat; :: thesis: ( j in dom (a * x) implies (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> )
assume A6: j in dom (a * x) ; :: thesis: (a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
then A7: j in dom x by A4, FINSEQ_3:31;
A8: ( len (ColVec2Mx x) = len x & width (ColVec2Mx x) = 1 & ( for j2 being Nat st j2 in dom x holds
(ColVec2Mx x) . j2 = <*(x . j2)*> ) ) by A1, Def9;
then A9: dom (ColVec2Mx x) = dom x by FINSEQ_3:31;
1 in Seg (width (MXR2MXF (ColVec2Mx x))) by A8, FINSEQ_1:3;
then A10: [j,1] in Indices (MXR2MXF (ColVec2Mx x)) by A7, A9, ZFMISC_1:106;
A11: j in dom (a * (ColVec2Mx x)) by A2, A4, A6, FINSEQ_3:31;
then (a * (ColVec2Mx x)) . j in rng (a * (ColVec2Mx x)) by FUNCT_1:def 5;
then reconsider q = (a * (ColVec2Mx x)) . j as FinSequence of REAL by FINSEQ_1:def 11;
consider s being FinSequence such that
A12: ( s in rng (a * (ColVec2Mx x)) & len s = width (a * (ColVec2Mx x)) ) by A1, A2, MATRIX_1:def 4;
consider n being Nat such that
A13: for x2 being set st x2 in rng (a * (ColVec2Mx x)) holds
ex s2 being FinSequence st
( s2 = x2 & len s2 = n ) by MATRIX_1:def 1;
q in rng (a * (ColVec2Mx x)) by A11, FUNCT_1:def 5;
then consider s2 being FinSequence such that
A14: ( s2 = q & len s2 = n ) by A13;
consider s3 being FinSequence such that
A15: ( s3 = s & len s3 = n ) by A12, A13;
A16: len q = width (ColVec2Mx x) by A12, A14, A15, Th27
.= 1 by A1, Def9
.= len <*((a * x) . j)*> by FINSEQ_1:57 ;
[j,1] in Indices (a * (ColVec2Mx x)) by A10, Th28;
then consider p being FinSequence of REAL such that
A17: ( p = (a * (ColVec2Mx x)) . j & (a * (ColVec2Mx x)) * j,1 = p . 1 ) by MATRIX_1:def 6;
consider p3 being FinSequence of REAL such that
A18: ( p3 = (ColVec2Mx x) . j & (ColVec2Mx x) * j,1 = p3 . 1 ) by A10, MATRIX_1:def 6;
A19: (ColVec2Mx x) . j = <*(x . j)*> by A1, A5, A6, Def9;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A20: q . 1 = a * ((ColVec2Mx x) * j,1) by A10, A17, Th29
.= a * (x . j) by A18, A19, FINSEQ_1:57
.= (a * x) . j by RVSUM_1:66
.= <*((a * x) . j)*> . 1 by FINSEQ_1:57 ;
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 )
assume A21: ( 1 <= i & i <= len <*((a * x) . j)*> ) ; :: thesis: q . i = <*((a * x) . j)*> . i
len <*((a * x) . j)*> = 1 by FINSEQ_1:57;
then i = 1 by A21, XXREAL_0:1;
hence q . i = <*((a * x) . j)*> . i by A20; :: thesis: verum

end;

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

end;

hence ColVec2Mx (a * x) = a * (ColVec2Mx x) by A1, A2, A3, A4, Def9; :: thesis: verum