let a be Real; 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; 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; ( 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
; ( 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
; for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q
let q be FinSequence of REAL ; ( q = A . i implies (a * A) . i = a * q )
assume A15:
q = A . i
; (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;
( 1 <= j & j <= len (a * q) implies qq . j = (a * q) . j )
assume
( 1
<= j &
j <= len (a * q) )
;
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;
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; verum