let a be Real; :: thesis: for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * ()
let x be FinSequence of REAL ; :: thesis: LineVec2Mx (a * x) = a * ()
A1: len (a * ()) = len () 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 * ()) * (1,j) = (a * x) . j
proof
len () = 1 by Def10;
then 1 in Seg (len ()) by FINSEQ_1:1;
then A5: 1 in dom () by FINSEQ_1:def 3;
1 in Seg (len (a * ())) by ;
then 1 in dom (a * ()) by FINSEQ_1:def 3;
then (a * ()) . 1 in rng (a * ()) by FUNCT_1:def 3;
then reconsider q = (a * ()) . 1 as FinSequence of REAL by FINSEQ_1:def 11;
let j be Nat; :: thesis: ( j in dom (a * x) implies (a * ()) * (1,j) = (a * x) . j )
A6: width () = len x by Def10;
A7: Indices (a * ()) = Indices () by Th28;
assume A8: j in dom (a * x) ; :: thesis: (a * ()) * (1,j) = (a * x) . j
then j in Seg (len x) by ;
then A9: [1,j] in Indices (a * ()) by ;
then A10: ex p being FinSequence of REAL st
( p = (a * ()) . 1 & (a * ()) * (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 * (() * (1,j)) by A7, A9, A10, Th29
.= a * (x . j) by
.= (a * x) . j by RVSUM_1:44 ;
hence (a * ()) * (1,j) = (a * x) . j by ; :: thesis: verum
end;
width (a * ()) = width () by Th27
.= len x by Def10 ;
hence LineVec2Mx (a * x) = a * () by A1, A2, A4, Def10; :: thesis: verum