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))
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 ;
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 ;
:: 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 ;
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 ;
:: 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;
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
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 ;
A15: [i,j] in Indices (AutMt (f2,b1,b2)) by ;
(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 ;
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 ;
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 ;
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
.= ((f1 + f2) . (b1 /. i)) |-- b2 by ;
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 ;
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 ;
A32: j in Seg (width (AutMt ((f1 + f2),b1,b2))) by ;
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 ;
then Seg (len b1) <> {} by FINSEQ_1:def 3;
then len b1 > 0 ;
then A34: j in Seg (len b2) by ;
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 ;
A37: j in dom b2 by ;
i in dom (AutMt (f2,b1,b2)) by ;
then A38: p3 = (AutMt (f2,b1,b2)) /. i by
.= (f2 . (b1 /. i)) |-- b2 by ;
then j in dom p3 by ;
then A39: (AutMt (f2,b1,b2)) * (i,j) = p3 /. j by ;
i in dom (AutMt (f1,b1,b2)) by ;
then A40: p2 = (AutMt (f1,b1,b2)) /. i by
.= (f1 . (b1 /. i)) |-- b2 by ;
then j in dom p2 by ;
then A41: (AutMt (f1,b1,b2)) * (i,j) = p2 /. j by ;
j <= len ((f2 . (b1 /. i)) |-- b2) by ;
then A42: p3 /. j = KL3 . (b2 /. j) by ;
j <= len ((f1 . (b1 /. i)) |-- b2) by ;
then A43: p2 /. j = KL2 . (b2 /. j) by ;
j in dom p1 by ;
hence (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j)) by ; :: thesis: verum
end;
hence (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) by ; :: thesis: verum
end;
len (AutMt ((f1 + f2),b1,b2)) = len ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) by ;
hence AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) by ; :: thesis: verum