let a be Real; :: thesis: for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)
let x be FinSequence of REAL ; :: thesis: LineVec2Mx (a * x) = a * (LineVec2Mx x)
A1: len (a * (LineVec2Mx x)) =
len (LineVec2Mx x)
by Th27
.=
1
by Def10
;
A2: width (a * (LineVec2Mx x)) =
width (LineVec2Mx x)
by Th27
.=
len x
by Def10
;
A3:
len (a * x) = len x
by EUCLID_2:8;
then A4:
dom (a * x) = dom x
by FINSEQ_3:31;
for j being Nat st j in dom (a * x) holds
(a * (LineVec2Mx x)) * 1,j = (a * x) . j
proof
let j be
Nat;
:: thesis: ( j in dom (a * x) implies (a * (LineVec2Mx x)) * 1,j = (a * x) . j )
assume A5:
j in dom (a * x)
;
:: thesis: (a * (LineVec2Mx x)) * 1,j = (a * x) . j
A6:
(
width (LineVec2Mx x) = len x &
len (LineVec2Mx x) = 1 & ( for
j2 being
Nat st
j2 in dom x holds
(LineVec2Mx x) * 1,
j2 = x . j2 ) )
by Def10;
then
1
in Seg (len (LineVec2Mx x))
by FINSEQ_1:3;
then A7:
1
in dom (LineVec2Mx x)
by FINSEQ_1:def 3;
1
in Seg (len (a * (LineVec2Mx x)))
by A1, FINSEQ_1:3;
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 5;
then reconsider q =
(a * (LineVec2Mx x)) . 1 as
FinSequence of
REAL by FINSEQ_1:def 11;
A8:
Indices (a * (LineVec2Mx x)) = Indices (LineVec2Mx x)
by Th28;
j in Seg (len x)
by A3, A5, FINSEQ_1:def 3;
then A9:
[1,j] in Indices (a * (LineVec2Mx x))
by A6, A7, A8, ZFMISC_1:106;
then consider p being
FinSequence of
REAL such that A10:
(
p = (a * (LineVec2Mx x)) . 1 &
(a * (LineVec2Mx x)) * 1,
j = p . j )
by MATRIX_1:def 6;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 13;
q . j =
a * ((LineVec2Mx x) * 1,j)
by A8, A9, A10, Th29
.=
a * (x . j)
by A4, A5, Def10
.=
(a * x) . j
by RVSUM_1:66
;
hence
(a * (LineVec2Mx x)) * 1,
j = (a * x) . j
by A10;
:: thesis: verum
end;
hence
LineVec2Mx (a * x) = a * (LineVec2Mx x)
by A1, A2, A3, Def10; :: thesis: verum