let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K

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 V1, V2 be finite-dimensional VectSp of K; :: 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 ;

then A2: dom (AutMt ((f1 + f2),b1,b2)) = dom (AutMt (f1,b1,b2)) by FINSEQ_3:29;

A3: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2))

len (AutMt (f1,b1,b2)) = len b1 by Def8

.= len (AutMt (f2,b1,b2)) by Def8 ;

then A10: dom (AutMt (f1,b1,b2)) = dom (AutMt (f2,b1,b2)) by FINSEQ_3:29;

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)

hence AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) by A9, A11, MATRIX_0:21; :: thesis: verum

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 V1, V2 be finite-dimensional VectSp of K; :: 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 ;

then A2: dom (AutMt ((f1 + f2),b1,b2)) = dom (AutMt (f1,b1,b2)) by FINSEQ_3:29;

A3: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2))

proof
end;

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

then A9:
width (AutMt ((f1 + f2),b1,b2)) = width ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)))
by MATRIX_3:def 3;per cases
( len b1 = 0 or len b1 > 0 )
;

end;

len (AutMt (f1,b1,b2)) = len b1 by Def8

.= len (AutMt (f2,b1,b2)) by Def8 ;

then A10: dom (AutMt (f1,b1,b2)) = dom (AutMt (f2,b1,b2)) by FINSEQ_3:29;

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

len (AutMt ((f1 + f2),b1,b2)) = len ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)))
by A1, MATRIX_3:def 3;
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 A13: [i,j] in [:(dom (AutMt ((f1 + f2),b1,b2))),(Seg (width (AutMt ((f1 + f2),b1,b2)))):] by MATRIX_0:def 4;

then A14: [i,j] in Indices (AutMt (f1,b1,b2)) by A2, A6, MATRIX_0:def 4;

A15: [i,j] in Indices (AutMt (f2,b1,b2)) by A10, A3, A2, A6, A13, MATRIX_0:def 4;

(AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j))

end;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 A13: [i,j] in [:(dom (AutMt ((f1 + f2),b1,b2))),(Seg (width (AutMt ((f1 + f2),b1,b2)))):] by MATRIX_0:def 4;

then A14: [i,j] in Indices (AutMt (f1,b1,b2)) by A2, A6, MATRIX_0:def 4;

A15: [i,j] in Indices (AutMt (f2,b1,b2)) by A10, A3, A2, A6, A13, MATRIX_0:def 4;

(AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j))

proof

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: verum
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 A13, ZFMISC_1:87;

then A21: i in dom b1 by Lm3;

reconsider b4 = rng b2 as Basis of V2 by Def2;

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_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;

( b4 is linearly-independent & (f1 + f2) . (b1 /. i) = (f1 . (b1 /. i)) + (f2 . (b1 /. i)) ) by Def3, VECTSP_7:def 3;

then A26: KL1 . (b2 /. j) = (KL2 + KL3) . (b2 /. j) by A24, A18, A16, Th6

.= (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 K 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 K 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 A13, 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 A13, ZFMISC_1:87;

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;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 A13, ZFMISC_1:87;

then A21: i in dom b1 by Lm3;

reconsider b4 = rng b2 as Basis of V2 by Def2;

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_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;

( b4 is linearly-independent & (f1 + f2) . (b1 /. i) = (f1 . (b1 /. i)) + (f2 . (b1 /. i)) ) by Def3, VECTSP_7:def 3;

then A26: KL1 . (b2 /. j) = (KL2 + KL3) . (b2 /. j) by A24, A18, A16, Th6

.= (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 K 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 K 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 A13, 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 A13, ZFMISC_1:87;

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

hence AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) by A9, A11, MATRIX_0:21; :: thesis: verum