let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 implies LineVec2Mx (x1 + x2) = () + () )
assume A1: len x1 = len x2 ; :: thesis: LineVec2Mx (x1 + x2) = () + ()
then A2: dom x1 = dom x2 by FINSEQ_3:29;
len (x1 + x2) = len x1 by ;
then A3: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A4: ( width () = len x1 & len () = 1 ) by Def10;
( width () = len x2 & len () = 1 ) by Def10;
then A5: Indices () = Indices () by ;
A6: Seg (width ()) = Seg (len x1) by Def10
.= dom x1 by FINSEQ_1:def 3 ;
A7: dom () = Seg (len ()) by FINSEQ_1:def 3
.= Seg 1 by Def10 ;
A8: ( width (LineVec2Mx (x1 + x2)) = len (x1 + x2) & len (LineVec2Mx (x1 + x2)) = 1 ) by Def10;
then A9: Indices (LineVec2Mx (x1 + x2)) = Indices () by ;
for i, j being Nat st [i,j] in Indices () holds
(LineVec2Mx (x1 + x2)) * (i,j) = (() * (i,j)) + (() * (i,j))
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices () implies (LineVec2Mx (x1 + x2)) * (i,j) = (() * (i,j)) + (() * (i,j)) )
assume A10: [i,j] in Indices () ; :: thesis: (LineVec2Mx (x1 + x2)) * (i,j) = (() * (i,j)) + (() * (i,j))
then consider q1 being FinSequence of REAL such that
q1 = () . i and
A11: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_0:def 5;
consider p being FinSequence of REAL such that
p = (LineVec2Mx (x1 + x2)) . i and
A12: (LineVec2Mx (x1 + x2)) * (i,j) = p . j by ;
consider q2 being FinSequence of REAL such that
q2 = () . i and
A13: (LineVec2Mx x2) * (i,j) = q2 . j by ;
A14: j in dom x1 by ;
i in Seg 1 by ;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A15: i = 1 by XXREAL_0:1;
then A16: q1 . j = x1 . j by ;
A17: q2 . j = x2 . j by A2, A14, A15, A13, Def10;
p . j = (x1 + x2) . j by A3, A14, A15, A12, Def10;
hence (LineVec2Mx (x1 + x2)) * (i,j) = (() * (i,j)) + (() * (i,j)) by ; :: thesis: verum
end;
hence LineVec2Mx (x1 + x2) = () + () by ; :: thesis: verum