let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A, B being Matrix of len b1, len B2,K holds Mx2Tran (A + B),b1,B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A, B being Matrix of len b1, len B2,K holds Mx2Tran (A + B),b1,B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for A, B being Matrix of len b1, len B2,K holds Mx2Tran (A + B),b1,B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)
let B2 be FinSequence of V2; :: thesis: for A, B being Matrix of len b1, len B2,K holds Mx2Tran (A + B),b1,B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)
let A, B be Matrix of len b1, len B2,K; :: thesis: Mx2Tran (A + B),b1,B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)
set AB = A + B;
set M = Mx2Tran (A + B),b1,B2;
set MA = Mx2Tran A,b1,B2;
set MB = Mx2Tran B,b1,B2;

now

let x be set ; :: thesis: ( x in the carrier of V1 implies (Mx2Tran (A + B),b1,B2) . x = ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x )
assume A1: x in the carrier of V1 ; :: thesis: (Mx2Tran (A + B),b1,B2) . x = ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x
reconsider v = x as Element of V1 by A1;

now

per cases ( len b1 = 0 or len b1 > 0 ) ;

suppose A2: len b1 = 0 ; :: thesis: (Mx2Tran (A + B),b1,B2) . x = ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x

hence (Mx2Tran (A + B),b1,B2) . x = 0. V2 by A1, Th33
.= (0. V2) + (0. V2) by RLVECT_1:def 7
.= ((Mx2Tran A,b1,B2) . v) + (0. V2) by A2, Th33
.= ((Mx2Tran A,b1,B2) . v) + ((Mx2Tran B,b1,B2) . v) by A2, Th33
.= ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x by MATRLIN:def 5 ;
:: thesis: verum

end;

suppose A3: len b1 > 0 ; :: thesis: (Mx2Tran (A + B),b1,B2) . x = ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x

set L = LineVec2Mx (v |-- b1);
A4: ( width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 ) by MATRIX_1:24, MATRLIN:def 9;
set mB = lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2;
A5: ( len B = len b1 & width B = len B2 ) by A3, MATRIX_1:24;
then A6: width ((LineVec2Mx (v |-- b1)) * B) = len B2 by A4, MATRIX_3:def 4;
then len (Line ((LineVec2Mx (v |-- b1)) * B),1) = len B2 by FINSEQ_1:def 18;
then dom (Line ((LineVec2Mx (v |-- b1)) * B),1) = dom B2 by FINSEQ_3:31;
then A7: dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) = dom B2 by MATRLIN:16;
then A8: len (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) = len B2 by FINSEQ_3:31;
A9: len A = len b1 by A3, MATRIX_1:24;
A10: len (LineVec2Mx (v |-- b1)) = 1 by MATRIX_1:24;
then A11: len ((LineVec2Mx (v |-- b1)) * A) = 1 by A9, A4, MATRIX_3:def 4;
set mA = lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2;
A12: width A = len B2 by A3, MATRIX_1:24;
then A13: width ((LineVec2Mx (v |-- b1)) * A) = len B2 by A9, A4, MATRIX_3:def 4;
then len (Line ((LineVec2Mx (v |-- b1)) * A),1) = len B2 by FINSEQ_1:def 18;
then dom (Line ((LineVec2Mx (v |-- b1)) * A),1) = dom B2 by FINSEQ_3:31;
then A14: dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = dom B2 by MATRLIN:16;
then A15: len (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = len B2 by FINSEQ_3:31;
A16: dom ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) = (dom B2) /\ (dom B2) by A14, A7, Lm3
.= dom B2 ;
then A17: len ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) = len B2 by FINSEQ_3:31;

A18: now

let k be Element of NAT ; :: thesis: ( k in dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) implies ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) . k = ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k) + ((lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) /. k) )
assume A19: k in dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) ; :: thesis: ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) . k = ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k) + ((lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) /. k)
( (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k = (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) . k & (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) /. k = (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) . k ) by A14, A7, A19, PARTFUN1:def 8;
hence ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) . k = ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k) + ((lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) /. k) by A14, A16, A19, FVSUM_1:21; :: thesis: verum

end;

thus (Mx2Tran (A + B),b1,B2) . x = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * (A + B)),1),B2) by Def3
.= Sum (lmlt (Line (((LineVec2Mx (v |-- b1)) * A) + ((LineVec2Mx (v |-- b1)) * B)),1),B2) by A3, A10, A9, A12, A5, A4, MATRIX_4:62
.= Sum (lmlt ((Line ((LineVec2Mx (v |-- b1)) * A),1) + (Line ((LineVec2Mx (v |-- b1)) * B),1)),B2) by A11, A13, A6, Lm5
.= Sum ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) by Th7
.= (Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2)) + (Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) by A15, A8, A17, A18, RLVECT_2:4
.= ((Mx2Tran A,b1,B2) . v) + (Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) by Def3
.= ((Mx2Tran A,b1,B2) . v) + ((Mx2Tran B,b1,B2) . v) by Def3
.= ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x by MATRLIN:def 5 ; :: thesis: verum

end;

end;

end;

hence (Mx2Tran (A + B),b1,B2) . x = ((Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)) . x ; :: thesis: verum

end;

hence Mx2Tran (A + B),b1,B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2) by FUNCT_2:18; :: thesis: verum