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: 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

.= len x by Def10 ;

hence LineVec2Mx (a * x) = a * (LineVec2Mx x) by A1, A2, A4, Def10; :: thesis: verum

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: 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

width (a * (LineVec2Mx x)) =
width (LineVec2Mx x)
by Th27
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; :: thesis: ( 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) ; :: thesis: (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; :: thesis: verum

end;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; :: thesis: ( 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) ; :: thesis: (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; :: thesis: verum

.= len x by Def10 ;

hence LineVec2Mx (a * x) = a * (LineVec2Mx x) by A1, A2, A4, Def10; :: thesis: verum