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:
len (AutMt f1,b1,b2) = len b1 by Def10
.= len (AutMt f2,b1,b2) by Def10 ;
then A1: dom (AutMt f1,b1,b2) = dom (AutMt f2,b1,b2) by FINSEQ_3:31;
A2: width (AutMt f1,b1,b2) = width (AutMt f2,b1,b2)

proof

per cases ;

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

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

end;

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

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

end;

A5: len (AutMt (f1 + f2),b1,b2) = len b1 by Def10
.= len (AutMt f1,b1,b2) by Def10 ;
then A6: len (AutMt (f1 + f2),b1,b2) = len ((AutMt f1,b1,b2) + (AutMt f2,b1,b2)) by MATRIX_3:def 3;
A7: dom (AutMt (f1 + f2),b1,b2) = dom (AutMt f1,b1,b2) by A5, FINSEQ_3:31;
A8: width (AutMt (f1 + f2),b1,b2) = width (AutMt f1,b1,b2)

proof

per cases ;

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

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

end;

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

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

end;

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

hence AutMt (f1 + f2),b1,b2 = (AutMt f1,b1,b2) + (AutMt f2,b1,b2) by A6, A11, MATRIX_1:21; :: thesis: