let a be Real; for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)
let x be FinSequence of REAL ; LineVec2Mx (a * x) = a * (LineVec2Mx x)
A1: len (a * (LineVec2Mx x)) =
len (LineVec2Mx x)
by Th27
.=
1
by Def10
;
A2:
len (a * x) = len x
by RVSUM_1:117;
then A3:
dom (a * x) = dom x
by FINSEQ_3:29;
A4:
for j being Nat st j in dom (a * x) holds
(a * (LineVec2Mx x)) * (1,j) = (a * x) . j
proof
len (LineVec2Mx x) = 1
by Def10;
then
1
in Seg (len (LineVec2Mx x))
by FINSEQ_1:1;
then A5:
1
in dom (LineVec2Mx x)
by FINSEQ_1:def 3;
1
in Seg (len (a * (LineVec2Mx x)))
by A1, FINSEQ_1:1;
then
1
in dom (a * (LineVec2Mx x))
by FINSEQ_1:def 3;
then
(a * (LineVec2Mx x)) . 1
in rng (a * (LineVec2Mx x))
by FUNCT_1:def 3;
then reconsider q =
(a * (LineVec2Mx x)) . 1 as
FinSequence of
REAL by FINSEQ_1:def 11;
let j be
Nat;
( j in dom (a * x) implies (a * (LineVec2Mx x)) * (1,j) = (a * x) . j )
A6:
width (LineVec2Mx x) = len x
by Def10;
A7:
Indices (a * (LineVec2Mx x)) = Indices (LineVec2Mx x)
by Th28;
assume A8:
j in dom (a * x)
;
(a * (LineVec2Mx x)) * (1,j) = (a * x) . j
then
j in Seg (len x)
by A2, FINSEQ_1:def 3;
then A9:
[1,j] in Indices (a * (LineVec2Mx x))
by A6, A5, A7, ZFMISC_1:87;
then A10:
ex
p being
FinSequence of
REAL st
(
p = (a * (LineVec2Mx x)) . 1 &
(a * (LineVec2Mx x)) * (1,
j)
= p . j )
by MATRIX_0:def 5;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
A11:
q . j in REAL
by XREAL_0:def 1;
q . j =
a * ((LineVec2Mx x) * (1,j))
by A7, A9, A10, Th29
.=
a * (x . j)
by A3, A8, Def10
.=
(a * x) . j
by RVSUM_1:44
;
hence
(a * (LineVec2Mx x)) * (1,
j)
= (a * x) . j
by A9, MATRIX_0:def 5, A11;
verum
end;
width (a * (LineVec2Mx x)) =
width (LineVec2Mx x)
by Th27
.=
len x
by Def10
;
hence
LineVec2Mx (a * x) = a * (LineVec2Mx x)
by A1, A2, A4, Def10; verum