let n, m be Nat; :: thesis: for f being n -element real-valued FinSequence
for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
let f be n -element real-valued FinSequence; :: thesis: for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
let M1, M2 be Matrix of n,m,F_Real; :: thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
set T12 = Mx2Tran (M1 + M2);
set T2 = Mx2Tran M2;
set T1 = Mx2Tran M1;

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

suppose A1: n <> 0 ; :: thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)

set L = LineVec2Mx (@ f);
len f = n by CARD_1:def 7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
A5: ( len M2 = n & width M2 = m ) by A1, MATRIX13:1;
then A6: width ((LineVec2Mx (@ f)) * M2) = m by A4, MATRIX_3:def 4;
A8: len M1 = n by A1, MATRIX13:1;
A9: width M1 = m by A1, MATRIX13:1;
then A10: width ((LineVec2Mx (@ f)) * M1) = m by A4, A8, MATRIX_3:def 4;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then len ((LineVec2Mx (@ f)) * M1) = 1 by A4, A8, MATRIX_3:def 4;
then B1: 1 in dom ((LineVec2Mx (@ f)) * M1) by FINSEQ_3:25;
( @ ((Mx2Tran M1) . f) = Line (((LineVec2Mx (@ f)) * M1),1) & @ ((Mx2Tran M2) . f) = Line (((LineVec2Mx (@ f)) * M2),1) ) by A1, Def3;
hence ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f) = (Line (((LineVec2Mx (@ f)) * M1),1)) + (Line (((LineVec2Mx (@ f)) * M2),1)) by RVSUM_1:def 4
.= Line ((((LineVec2Mx (@ f)) * M1) + ((LineVec2Mx (@ f)) * M2)),1) by B1, A10, A6, MATRIX_4:59
.= Line (((LineVec2Mx (@ f)) * (M1 + M2)),1) by A4, A8, A9, A5, MATRIX_4:62
.= (Mx2Tran (M1 + M2)) . f by A1, Def3 ;
:: thesis: verum

end;

suppose A13: n = 0 ; :: thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)

A14: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
then A15: (Mx2Tran M2) . f = m |-> 0 by A13, Def3;
thus (Mx2Tran (M1 + M2)) . f = m |-> (zz + zz) by A13, A14, Def3
.= (m |-> zz) + (m |-> zz) by RVSUM_1:14
.= ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f) by A13, A14, A15, Def3 ; :: thesis: verum

end;

end;