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 :: thesis: for x being object st x in the carrier of V1 holds
(Mx2Tran ((A + B),b1,B2)) . x = ((Mx2Tran (A,b1,B2)) + (Mx2Tran (B,b1,B2))) . x

let x be object ; :: 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 :: thesis: (Mx2Tran ((A + B),b1,B2)) . x = ((Mx2Tran (A,b1,B2)) + (Mx2Tran (B,b1,B2))) . x

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 4
.= ((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 3 ;
:: 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_0:23, MATRLIN:def 7;
set mB = lmlt ((Line (((LineVec2Mx (v |-- b1)) * B),1)),B2);
A5: ( len B = len b1 & width B = len B2 ) by A3, MATRIX_0:23;
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 CARD_1:def 7;
then dom (Line (((LineVec2Mx (v |-- b1)) * B),1)) = dom B2 by FINSEQ_3:29;
then A7: dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * B),1)),B2)) = dom B2 by MATRLIN:12;
then A8: len (lmlt ((Line (((LineVec2Mx (v |-- b1)) * B),1)),B2)) = len B2 by FINSEQ_3:29;
A9: len A = len b1 by A3, MATRIX_0:23;
len (LineVec2Mx (v |-- b1)) = 1 by MATRIX_0:23;
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_0:23;
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 CARD_1:def 7;
then dom (Line (((LineVec2Mx (v |-- b1)) * A),1)) = dom B2 by FINSEQ_3:29;
then A14: dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) = dom B2 by MATRLIN:12;
then A15: len (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) = len B2 by FINSEQ_3:29;
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:29;

A18: now :: thesis: for k being Nat st k in dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) holds
((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)

let k be 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 6;
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:17; :: 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 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:2
.= ((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 3 ; :: 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:12; :: thesis: verum