let a be Real; for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)
let x be FinSequence of REAL ; ( len x > 0 implies ColVec2Mx (a * x) = a * (ColVec2Mx x) )
assume A1:
len x > 0
; 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
len (ColVec2Mx x) = len x
by A1, Def9;
then A6:
dom (ColVec2Mx x) = dom x
by FINSEQ_3:29;
let j be
Nat;
( 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)
;
(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
hence
(a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
by A14, FINSEQ_1:14;
verum
end;
width (a * (ColVec2Mx x)) =
width (ColVec2Mx x)
by Th27
.=
1
by A1, Def9
;
hence
ColVec2Mx (a * x) = a * (ColVec2Mx x)
by A1, A2, A3, A5, Def9; verum