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

proof

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;

ex s2 being FinSequence st
( 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