let V1, V2 be free finite-rank Z_Module; :: thesis: for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let f1, f2 be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
let b2 be OrdBasis of V2; :: thesis: AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))
A1: len (AutMt ((f1 + f2),b1,b2)) = len b1 by Def8
.= len (AutMt (f1,b1,b2)) by Def8 ;
A3: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2))

proof

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

suppose A4: len b1 = 0 ; :: thesis: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2))

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

end;

suppose A5: len b1 > 0 ; :: thesis: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2))

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

end;

end;

end;

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

proof

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

suppose A7: len b1 = 0 ; :: thesis: width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2))

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

end;

suppose A8: len b1 > 0 ; :: thesis: width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2))

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

end;

end;

end;

then A9: width (AutMt ((f1 + f2),b1,b2)) = width ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) by MATRIX_3:def 3;
AX10: len (AutMt (f1,b1,b2)) = len b1 by Def8
.= len (AutMt (f2,b1,b2)) by Def8 ;
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: ( [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) implies (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) )
assume A12: [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) ; :: thesis: (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j)
then A14: [i,j] in Indices (AutMt (f1,b1,b2)) by A1, A6, FINSEQ_3:29;
A15: [i,j] in Indices (AutMt (f2,b1,b2)) by A1, A3, A6, AX10, A12, FINSEQ_3:29;
A15A: (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 Def7;
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 Def7;
A20: i in dom (AutMt ((f1 + f2),b1,b2)) by A12, ZFMISC_1:87;
then A21: i in dom b1 by Lm3;
reconsider b4 = rng b2 as Basis of V2 by defOrdBasis;
consider p1 being FinSequence of INT.Ring such that
A22: p1 = (AutMt ((f1 + f2),b1,b2)) . i and
A23: (AutMt ((f1 + f2),b1,b2)) * (i,j) = p1 . j by A12, MATRIX_0:def 5;
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 Def7;
Z: b4 is linearly-independent by VECTSP_7:def 3;
(f1 + f2) . (b1 /. i) = (f1 . (b1 /. i)) + (f2 . (b1 /. i)) by MATRLIN:def 3;
then A26: KL1 . (b2 /. j) = (KL2 + KL3) . (b2 /. j) by A24, A18, A16, Th6, Z
.= (KL2 . (b2 /. j)) + (KL3 . (b2 /. j)) by VECTSP_6:22 ;
A27: p1 = (AutMt ((f1 + f2),b1,b2)) /. i by A22, A20, PARTFUN1:def 6
.= ((f1 + f2) . (b1 /. i)) |-- b2 by A21, Def8 ;
consider p3 being FinSequence of INT.Ring such that
A28: p3 = (AutMt (f2,b1,b2)) . i and
A29: (AutMt (f2,b1,b2)) * (i,j) = p3 . j by A15, MATRIX_0:def 5;
consider p2 being FinSequence of INT.Ring such that
A30: p2 = (AutMt (f1,b1,b2)) . i and
A31: (AutMt (f1,b1,b2)) * (i,j) = p2 . j by A14, MATRIX_0:def 5;
A32: j in Seg (width (AutMt ((f1 + f2),b1,b2))) by A12, ZFMISC_1:87;
then A33: 1 <= j by FINSEQ_1:1;
len b1 = len (AutMt ((f1 + f2),b1,b2)) by Def8;
then dom b1 = dom (AutMt ((f1 + f2),b1,b2)) by FINSEQ_3:29;
then dom b1 <> {} by A12;
then Seg (len b1) <> {} by FINSEQ_1:def 3;
then len b1 > 0 ;
then A34: j in Seg (len b2) by A32, Th39;
then A35: j <= len b2 by FINSEQ_1:1;
then j <= len (((f1 + f2) . (b1 /. i)) |-- b2) by Def7;
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 6
.= (f2 . (b1 /. i)) |-- b2 by A21, Def8 ;
then j in dom p3 by A37, Lm1;
then A39: (AutMt (f2,b1,b2)) * (i,j) = p3 /. j by A29, PARTFUN1:def 6;
i in dom (AutMt (f1,b1,b2)) by A21, Lm3;
then A40: p2 = (AutMt (f1,b1,b2)) /. i by A30, PARTFUN1:def 6
.= (f1 . (b1 /. i)) |-- b2 by A21, Def8 ;
then j in dom p2 by A37, Lm1;
then A41: (AutMt (f1,b1,b2)) * (i,j) = p2 /. j by A31, PARTFUN1:def 6;
j <= len ((f2 . (b1 /. i)) |-- b2) by A35, Def7;
then A42: p3 /. j = KL3 . (b2 /. j) by A33, A38, A17;
j <= len ((f1 . (b1 /. i)) |-- b2) by A35, Def7;
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 6; :: thesis: verum

end;

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

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_0:21; :: thesis: verum