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 A1:
( len A > 0 & 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 ) )
A2:
( len (a * A) = len A & width (a * A) = width A )
by Th27;
then A3:
dom (a * A) = dom A
by FINSEQ_3:31;
consider n being Nat such that
A4:
for x being set st x in rng A holds
ex p being FinSequence of REAL st
( x = p & len p = n )
by MATRIX_1:9;
A . i in rng A
by A1, FUNCT_1:def 5;
then consider p2 being FinSequence of REAL such that
A5:
( A . i = p2 & len p2 = n )
by A4;
thus
ex p being FinSequence of REAL st p = A . i
by A5; :: 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 A6:
q = A . i
; :: thesis: (a * A) . i = a * q
( len (a * A) = len A & width (a * A) = width A & ( for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * i2,j2 = a * (A * i2,j2) ) )
by Th27, Th29;
then consider s being FinSequence such that
A7:
( s in rng (a * A) & len s = width (a * A) )
by A1, MATRIX_1:def 4;
consider s3 being FinSequence such that
A8:
( s3 in rng A & len s3 = width A )
by A1, MATRIX_1:def 4;
consider n2 being Nat such that
A9:
for x being set st x in rng (a * A) holds
ex s2 being FinSequence st
( s2 = x & len s2 = n2 )
by MATRIX_1:def 1;
consider n3 being Nat such that
A10:
for x being set st x in rng A holds
ex s2 being FinSequence st
( s2 = x & len s2 = n3 )
by MATRIX_1:def 1;
consider s2 being FinSequence such that
A11:
( s2 = s & len s2 = n2 )
by A7, A9;
consider s4 being FinSequence such that
A12:
( s4 = s3 & len s4 = n3 )
by A8, A10;
(a * A) . i in rng (a * A)
by A1, A3, FUNCT_1:def 5;
then consider qq being FinSequence such that
A13:
( qq = (a * A) . i & len qq = n2 )
by A9;
A . i in rng A
by A1, FUNCT_1:def 5;
then consider qq0 being FinSequence such that
A14:
( qq0 = A . i & len qq0 = n3 )
by A10;
A15:
len (a * q) = width A
by A6, A8, A12, A14, EUCLID_2:8;
A16:
width A = len qq
by A7, A11, A13, Th27;
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 A17:
j in Seg (width A)
by A15, FINSEQ_1:3;
then A18:
[i,j] in Indices A
by A1, ZFMISC_1:106;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 13;
[i,j] in Indices (a * A)
by A1, A2, A3, A17, ZFMISC_1:106;
then consider p being
FinSequence of
REAL such that A19:
(
p = (a * A) . i &
(a * A) * i,
j = p . j )
by MATRIX_1:def 6;
consider p2 being
FinSequence of
REAL such that A20:
(
p2 = A . i &
A * i,
j = p2 . j )
by A18, MATRIX_1:def 6;
qq . j = a * (q . j)
by A6, A13, A18, A19, A20, Th29;
hence
qq . j = (a * q) . j
by RVSUM_1:66;
:: thesis: verum
end;
hence
(a * A) . i = a * q
by A13, A15, A16, FINSEQ_1:18; :: thesis: verum