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);
set mA = lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2;
set mB = lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2;
A4: ( len (LineVec2Mx (v |-- b1)) = 1 & len A = len b1 & len B = len b1 & width A = len B2 & width B = len B2 & width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 ) by A3, MATRIX_1:24, MATRLIN:def 9;
then A5: ( len ((LineVec2Mx (v |-- b1)) * A) = 1 & width ((LineVec2Mx (v |-- b1)) * A) = len B2 & len ((LineVec2Mx (v |-- b1)) * B) = 1 & width ((LineVec2Mx (v |-- b1)) * B) = len B2 ) by MATRIX_3:def 4;
then ( len (Line ((LineVec2Mx (v |-- b1)) * A),1) = len B2 & len (Line ((LineVec2Mx (v |-- b1)) * B),1) = len B2 ) by FINSEQ_1:def 18;
then ( dom (Line ((LineVec2Mx (v |-- b1)) * A),1) = dom B2 & dom (Line ((LineVec2Mx (v |-- b1)) * B),1) = dom B2 ) by FINSEQ_3:31;
then A6: ( dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = dom B2 & dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) = dom B2 ) by MATRLIN:16;
then A7: ( len (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = len B2 & len (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2) = len B2 ) by FINSEQ_3:31;
A8: dom ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) = (dom B2) /\ (dom B2) by A6, Lm3
.= dom B2 ;
then A9: len ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) + (lmlt (Line ((LineVec2Mx (v |-- b1)) * B),1),B2)) = len B2 by FINSEQ_3:31;

A10: 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 A11: 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 A6, A11, 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 A6, A8, A11, 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, A4, MATRIX_4:62
.= Sum (lmlt ((Line ((LineVec2Mx (v |-- b1)) * A),1) + (Line ((LineVec2Mx (v |-- b1)) * B),1)),B2) by A5, 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 A7, A9, A10, 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