let n, m be Nat; :: thesis: for f1, f2 being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
let f1, f2 be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
let M be Matrix of n,m,F_Real; :: thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
set f12 = f1 + f2;
set T = Mx2Tran M;

per cases ( n <> 0 or n = 0 ) ;

suppose A1: n <> 0 ; :: thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)

A4: len M = n by A1, MATRIX13:1;
set L2 = LineVec2Mx (@ f2);
set L1 = LineVec2Mx (@ f1);
A5: len (LineVec2Mx (@ f2)) = 1 by MATRIX13:1;
A6: len f2 = n by CARD_1:def 7;
then A7: width (LineVec2Mx (@ f2)) = n by MATRIX13:1;
A8: width M = m by A1, MATRIX13:1;
then A9: width ((LineVec2Mx (@ f2)) * M) = m by A7, A4, MATRIX_3:def 4;
A10: len f1 = n by CARD_1:def 7;
then A11: width (LineVec2Mx (@ f1)) = n by MATRIX13:1;
then A12: width ((LineVec2Mx (@ f1)) * M) = m by A4, A8, MATRIX_3:def 4;
A13: len (LineVec2Mx (@ f1)) = 1 by MATRIX13:1;
then a13: len ((LineVec2Mx (@ f1)) * M) = 1 by A11, A4, MATRIX_3:def 4;
A15: ( @ ((Mx2Tran M) . f1) = Line (((LineVec2Mx (@ f1)) * M),1) & @ ((Mx2Tran M) . f2) = Line (((LineVec2Mx (@ f2)) * M),1) ) by A1, Def3;
B1: 1 in dom ((LineVec2Mx (@ f1)) * M) by a13, FINSEQ_3:25;
@ (f1 + f2) = (@ f1) + (@ f2) by RVSUM_1:def 4;
then (LineVec2Mx (@ (f1 + f2))) * M = ((LineVec2Mx (@ f1)) + (LineVec2Mx (@ f2))) * M by A10, A6, MATRIX15:27
.= ((LineVec2Mx (@ f1)) * M) + ((LineVec2Mx (@ f2)) * M) by A13, A5, A11, A7, A4, MATRIX_4:63 ;
hence (Mx2Tran M) . (f1 + f2) = Line ((((LineVec2Mx (@ f1)) * M) + ((LineVec2Mx (@ f2)) * M)),1) by A1, Def3
.= (Line (((LineVec2Mx (@ f1)) * M),1)) + (Line (((LineVec2Mx (@ f2)) * M),1)) by B1, A12, A9, MATRIX_4:59
.= ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2) by A15, RVSUM_1:def 4 ;
:: thesis: verum

end;

suppose A16: n = 0 ; :: thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)

reconsider zz = 0 as Real ;
A17: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
then A18: (Mx2Tran M) . f2 = m |-> 0 by A16, Def3;
thus (Mx2Tran M) . (f1 + f2) = m |-> (zz + zz) by A16, A17, Def3
.= (m |-> zz) + (m |-> zz) by RVSUM_1:14
.= ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2) by A16, A18 ; :: thesis: verum

end;

end;