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)*>

.= 1 by A1, Def9 ;

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

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

width (a * (ColVec2Mx x)) =
width (ColVec2Mx x)
by Th27
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, FINSEQ_1:40

.= (a * x) . j by RVSUM_1:44

.= <*((a * x) . j)*> . 1 by FINSEQ_1:40 ;

for i being Nat st 1 <= i & i <= len <*((a * x) . j)*> holds

q . i = <*((a * x) . j)*> . i

end;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, FINSEQ_1:40

.= (a * x) . j by RVSUM_1:44

.= <*((a * x) . j)*> . 1 by FINSEQ_1:40 ;

for i being Nat st 1 <= i & i <= len <*((a * x) . j)*> holds

q . i = <*((a * x) . j)*> . i

proof

hence
(a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
by A14, FINSEQ_1:14; :: thesis: verum
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;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

.= 1 by A1, Def9 ;

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