let K be Field; :: thesis:
let V1, V2 be finite-dimensional VectSp of K; :: thesis:
let f1, f2 be Function of V1,V2; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let b2 be OrdBasis of V2; :: thesis:
A1: len (AutMt (f1 + f2),b1,b2) = len b1 by Def10
.= len (AutMt f1,b1,b2) by Def10 ;
then A2: dom (AutMt (f1 + f2),b1,b2) = dom (AutMt f1,b1,b2) by FINSEQ_3:31;
A3: width (AutMt f1,b1,b2) = width (AutMt f2,b1,b2)

proof

per cases ;

suppose A4: len b1 = 0 ; :: thesis:

then AutMt f1,b1,b2 = {} by Th43
.= AutMt f2,b1,b2 by A4, Th43 ;
hence width (AutMt f1,b1,b2) = width (AutMt f2,b1,b2) ; :: thesis:

end;

suppose A5: len b1 > 0 ; :: thesis:

hence width (AutMt f1,b1,b2) = len b2 by Th44
.= width (AutMt f2,b1,b2) by A5, Th44 ;
:: thesis:

end;

A6: width (AutMt (f1 + f2),b1,b2) = width (AutMt f1,b1,b2)

proof

per cases ;

suppose A7: len b1 = 0 ; :: thesis:

then AutMt (f1 + f2),b1,b2 = {} by Th43
.= AutMt f1,b1,b2 by A7, Th43 ;
hence width (AutMt (f1 + f2),b1,b2) = width (AutMt f1,b1,b2) ; :: thesis:

end;

suppose A8: len b1 > 0 ; :: thesis:

hence width (AutMt (f1 + f2),b1,b2) = len b2 by Th44
.= width (AutMt f1,b1,b2) by A8, Th44 ;
:: thesis:

end;

then A9: width (AutMt (f1 + f2),b1,b2) = width ((AutMt f1,b1,b2) + (AutMt f2,b1,b2)) by MATRIX_3:def 3;
len (AutMt f1,b1,b2) = len b1 by Def10
.= len (AutMt f2,b1,b2) by Def10 ;
then A10: dom (AutMt f1,b1,b2) = dom (AutMt f2,b1,b2) by FINSEQ_3:31;
A11: for i, j being Nat st [i,j] in Indices (AutMt (f1 + f2),b1,b2) holds
(AutMt (f1 + f2),b1,b2) * i,j = ((AutMt f1,b1,b2) + (AutMt f2,b1,b2)) * i,j

proof

let i, j be Nat; :: thesis:
assume A12: [i,j] in Indices (AutMt (f1 + f2),b1,b2) ; :: thesis:
then A13: [i,j] in [:(dom (AutMt (f1 + f2),b1,b2)),(Seg (width (AutMt (f1 + f2),b1,b2))):] by MATRIX_1:def 5;
then A14: [i,j] in Indices (AutMt f1,b1,b2) by A2, A6, MATRIX_1:def 5;
A15: [i,j] in Indices (AutMt f2,b1,b2) by A10, A3, A2, A6, A13, MATRIX_1:def 5;
(AutMt (f1 + f2),b1,b2) * i,j = ((AutMt f1,b1,b2) * i,j) + ((AutMt f2,b1,b2) * i,j)

proof

consider KL3 being Linear_Combination of V2 such that
A16: ( f2 . (b1 /. i) = Sum KL3 & Carrier KL3 c= rng b2 ) and
A17: for t being Nat st 1 <= t & t <= len ((f2 . (b1 /. i)) |-- b2) holds
((f2 . (b1 /. i)) |-- b2) /. t = KL3 . (b2 /. t) by Def9;
consider KL2 being Linear_Combination of V2 such that
A18: ( f1 . (b1 /. i) = Sum KL2 & Carrier KL2 c= rng b2 ) and
A19: for t being Nat st 1 <= t & t <= len ((f1 . (b1 /. i)) |-- b2) holds
((f1 . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t) by Def9;
A20: i in dom (AutMt (f1 + f2),b1,b2) by A13, ZFMISC_1:106;
then A21: i in dom b1 by Lm3;
reconsider b4 = rng b2 as Basis of V2 by Def4;
consider p1 being FinSequence of K such that
A22: p1 = (AutMt (f1 + f2),b1,b2) . i and
A23: (AutMt (f1 + f2),b1,b2) * i,j = p1 . j by A12, MATRIX_1:def 6;
consider KL1 being Linear_Combination of V2 such that
A24: ( (f1 + f2) . (b1 /. i) = Sum KL1 & Carrier KL1 c= rng b2 ) and
A25: for t being Nat st 1 <= t & t <= len (((f1 + f2) . (b1 /. i)) |-- b2) holds
(((f1 + f2) . (b1 /. i)) |-- b2) /. t = KL1 . (b2 /. t) by Def9;
( b4 is linearly-independent & (f1 + f2) . (b1 /. i) = (f1 . (b1 /. i)) + (f2 . (b1 /. i)) ) by Def5, VECTSP_7:def 3;
then A26: KL1 . (b2 /. j) = (KL2 + KL3) . (b2 /. j) by A24, A18, A16, Th10
.= (KL2 . (b2 /. j)) + (KL3 . (b2 /. j)) by VECTSP_6:def 11 ;
A27: p1 = (AutMt (f1 + f2),b1,b2) /. i by A22, A20, PARTFUN1:def 8
.= ((f1 + f2) . (b1 /. i)) |-- b2 by A21, Def10 ;
consider p3 being FinSequence of K such that
A28: p3 = (AutMt f2,b1,b2) . i and
A29: (AutMt f2,b1,b2) * i,j = p3 . j by A15, MATRIX_1:def 6;
consider p2 being FinSequence of K such that
A30: p2 = (AutMt f1,b1,b2) . i and
A31: (AutMt f1,b1,b2) * i,j = p2 . j by A14, MATRIX_1:def 6;
A32: j in Seg (width (AutMt (f1 + f2),b1,b2)) by A13, ZFMISC_1:106;
then A33: 1 <= j by FINSEQ_1:3;
len b1 = len (AutMt (f1 + f2),b1,b2) by Def10;
then dom b1 = dom (AutMt (f1 + f2),b1,b2) by FINSEQ_3:31;
then dom b1 <> {} by A13, ZFMISC_1:106;
then Seg (len b1) <> {} by FINSEQ_1:def 3;
then len b1 > 0 ;
then A34: j in Seg (len b2) by A32, Th44;
then A35: j <= len b2 by FINSEQ_1:3;
then j <= len (((f1 + f2) . (b1 /. i)) |-- b2) by Def9;
then A36: p1 /. j = KL1 . (b2 /. j) by A33, A27, A25;
A37: j in dom b2 by A34, FINSEQ_1:def 3;
i in dom (AutMt f2,b1,b2) by A21, Lm3;
then A38: p3 = (AutMt f2,b1,b2) /. i by A28, PARTFUN1:def 8
.= (f2 . (b1 /. i)) |-- b2 by A21, Def10 ;
then j in dom p3 by A37, Lm1;
then A39: (AutMt f2,b1,b2) * i,j = p3 /. j by A29, PARTFUN1:def 8;
i in dom (AutMt f1,b1,b2) by A21, Lm3;
then A40: p2 = (AutMt f1,b1,b2) /. i by A30, PARTFUN1:def 8
.= (f1 . (b1 /. i)) |-- b2 by A21, Def10 ;
then j in dom p2 by A37, Lm1;
then A41: (AutMt f1,b1,b2) * i,j = p2 /. j by A31, PARTFUN1:def 8;
j <= len ((f2 . (b1 /. i)) |-- b2) by A35, Def9;
then A42: p3 /. j = KL3 . (b2 /. j) by A33, A38, A17;
j <= len ((f1 . (b1 /. i)) |-- b2) by A35, Def9;
then A43: p2 /. j = KL2 . (b2 /. j) by A33, A40, A19;
j in dom p1 by A37, A27, Lm1;
hence (AutMt (f1 + f2),b1,b2) * i,j = ((AutMt f1,b1,b2) * i,j) + ((AutMt f2,b1,b2) * i,j) by A23, A41, A39, A36, A43, A42, A26, PARTFUN1:def 8; :: thesis:

end;

hence (AutMt (f1 + f2),b1,b2) * i,j = ((AutMt f1,b1,b2) + (AutMt f2,b1,b2)) * i,j by A14, MATRIX_3:def 3; :: thesis:

end;

len (AutMt (f1 + f2),b1,b2) = len ((AutMt f1,b1,b2) + (AutMt f2,b1,b2)) by A1, MATRIX_3:def 3;
hence AutMt (f1 + f2),b1,b2 = (AutMt f1,b1,b2) + (AutMt f2,b1,b2) by A9, A11, MATRIX_1:21; :: thesis: