let a be Real; :: thesis: for i being Nat

for A being Matrix of REAL st len A > 0 & i in dom A holds

( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

let i be Nat; :: thesis: for A being Matrix of REAL st len A > 0 & i in dom A holds

( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

let A be Matrix of REAL; :: thesis: ( len A > 0 & i in dom A implies ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) ) )

assume that

A1: len A > 0 and

A2: i in dom A ; :: thesis: ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

consider n3 being Nat such that

A3: for x being object st x in rng A holds

ex s2 being FinSequence st

( s2 = x & len s2 = n3 ) by MATRIX_0:def 1;

A . i in rng A by A2, FUNCT_1:def 3;

then A4: ex qq0 being FinSequence st

( qq0 = A . i & len qq0 = n3 ) by A3;

len (a * A) = len A by Th27;

then consider s being FinSequence such that

A5: s in rng (a * A) and

A6: len s = width (a * A) by A1, MATRIX_0:def 3;

A7: width (a * A) = width A by Th27;

consider s3 being FinSequence such that

A8: s3 in rng A and

A9: len s3 = width A by A1, MATRIX_0:def 3;

consider n2 being Nat such that

A10: for x being object st x in rng (a * A) holds

ex s2 being FinSequence st

( s2 = x & len s2 = n2 ) by MATRIX_0:def 1;

len (a * A) = len A by Th27;

then A11: dom (a * A) = dom A by FINSEQ_3:29;

then (a * A) . i in rng (a * A) by A2, FUNCT_1:def 3;

then consider qq being FinSequence such that

A12: qq = (a * A) . i and

A13: len qq = n2 by A10;

consider n being Nat such that

A14: for x being object st x in rng A holds

ex p being FinSequence of REAL st

( x = p & len p = n ) by MATRIX_0:9;

A . i in rng A by A2, FUNCT_1:def 3;

then ex p2 being FinSequence of REAL st

( A . i = p2 & len p2 = n ) by A14;

hence ex p being FinSequence of REAL st p = A . i ; :: thesis: for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q

let q be FinSequence of REAL ; :: thesis: ( q = A . i implies (a * A) . i = a * q )

assume A15: q = A . i ; :: thesis: (a * A) . i = a * q

A16: ex s4 being FinSequence st

( s4 = s3 & len s4 = n3 ) by A8, A3;

then A17: len (a * q) = width A by A15, A9, A4, RVSUM_1:117;

A18: for j being Nat st 1 <= j & j <= len (a * q) holds

qq . j = (a * q) . j

( s2 = s & len s2 = n2 ) by A5, A10;

then width A = len qq by A6, A13, Th27;

hence (a * A) . i = a * q by A15, A9, A16, A12, A4, A18, FINSEQ_1:14, RVSUM_1:117; :: thesis: verum

for A being Matrix of REAL st len A > 0 & i in dom A holds

( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

let i be Nat; :: thesis: for A being Matrix of REAL st len A > 0 & i in dom A holds

( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

let A be Matrix of REAL; :: thesis: ( len A > 0 & i in dom A implies ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) ) )

assume that

A1: len A > 0 and

A2: i in dom A ; :: thesis: ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q ) )

consider n3 being Nat such that

A3: for x being object st x in rng A holds

ex s2 being FinSequence st

( s2 = x & len s2 = n3 ) by MATRIX_0:def 1;

A . i in rng A by A2, FUNCT_1:def 3;

then A4: ex qq0 being FinSequence st

( qq0 = A . i & len qq0 = n3 ) by A3;

len (a * A) = len A by Th27;

then consider s being FinSequence such that

A5: s in rng (a * A) and

A6: len s = width (a * A) by A1, MATRIX_0:def 3;

A7: width (a * A) = width A by Th27;

consider s3 being FinSequence such that

A8: s3 in rng A and

A9: len s3 = width A by A1, MATRIX_0:def 3;

consider n2 being Nat such that

A10: for x being object st x in rng (a * A) holds

ex s2 being FinSequence st

( s2 = x & len s2 = n2 ) by MATRIX_0:def 1;

len (a * A) = len A by Th27;

then A11: dom (a * A) = dom A by FINSEQ_3:29;

then (a * A) . i in rng (a * A) by A2, FUNCT_1:def 3;

then consider qq being FinSequence such that

A12: qq = (a * A) . i and

A13: len qq = n2 by A10;

consider n being Nat such that

A14: for x being object st x in rng A holds

ex p being FinSequence of REAL st

( x = p & len p = n ) by MATRIX_0:9;

A . i in rng A by A2, FUNCT_1:def 3;

then ex p2 being FinSequence of REAL st

( A . i = p2 & len p2 = n ) by A14;

hence ex p being FinSequence of REAL st p = A . i ; :: thesis: for q being FinSequence of REAL st q = A . i holds

(a * A) . i = a * q

let q be FinSequence of REAL ; :: thesis: ( q = A . i implies (a * A) . i = a * q )

assume A15: q = A . i ; :: thesis: (a * A) . i = a * q

A16: ex s4 being FinSequence st

( s4 = s3 & len s4 = n3 ) by A8, A3;

then A17: len (a * q) = width A by A15, A9, A4, RVSUM_1:117;

A18: for j being Nat st 1 <= j & j <= len (a * q) holds

qq . j = (a * q) . j

proof

ex s2 being FinSequence st
let j be Nat; :: thesis: ( 1 <= j & j <= len (a * q) implies qq . j = (a * q) . j )

assume ( 1 <= j & j <= len (a * q) ) ; :: thesis: qq . j = (a * q) . j

then A19: j in Seg (width A) by A17, FINSEQ_1:1;

then A20: [i,j] in Indices A by A2, ZFMISC_1:87;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

[i,j] in Indices (a * A) by A2, A7, A11, A19, ZFMISC_1:87;

then A21: ex p being FinSequence of REAL st

( p = (a * A) . i & (a * A) * (i,j) = p . j ) by MATRIX_0:def 5;

ex p2 being FinSequence of REAL st

( p2 = A . i & A * (i,j) = p2 . j ) by A20, MATRIX_0:def 5;

then qq . j = a * (q . j) by A15, A12, A20, A21, Th29;

hence qq . j = (a * q) . j by RVSUM_1:44; :: thesis: verum

end;assume ( 1 <= j & j <= len (a * q) ) ; :: thesis: qq . j = (a * q) . j

then A19: j in Seg (width A) by A17, FINSEQ_1:1;

then A20: [i,j] in Indices A by A2, ZFMISC_1:87;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

[i,j] in Indices (a * A) by A2, A7, A11, A19, ZFMISC_1:87;

then A21: ex p being FinSequence of REAL st

( p = (a * A) . i & (a * A) * (i,j) = p . j ) by MATRIX_0:def 5;

ex p2 being FinSequence of REAL st

( p2 = A . i & A * (i,j) = p2 . j ) by A20, MATRIX_0:def 5;

then qq . j = a * (q . j) by A15, A12, A20, A21, Th29;

hence qq . j = (a * q) . j by RVSUM_1:44; :: thesis: verum

( s2 = s & len s2 = n2 ) by A5, A10;

then width A = len qq by A6, A13, Th27;

hence (a * A) . i = a * q by A15, A9, A16, A12, A4, A18, FINSEQ_1:14, RVSUM_1:117; :: thesis: verum