let K be Field; :: thesis: for a being Element of K

for V1, V2 being finite-dimensional VectSp of K

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

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

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

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

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

let b2 be OrdBasis of V2; :: thesis: ( a <> 0. K implies AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) )

assume A1: a <> 0. K ; :: thesis: AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

A2: width (AutMt ((a * f),b1,b2)) = width (AutMt (f,b1,b2))

A6: len (AutMt ((a * f),b1,b2)) = len b1 by Def8

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

then A7: dom (AutMt ((a * f),b1,b2)) = dom (AutMt (f,b1,b2)) by FINSEQ_3:29;

A8: for i, j being Nat st [i,j] in Indices (AutMt ((a * f),b1,b2)) holds

(AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j)

hence AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) by A5, A8, MATRIX_0:21; :: thesis: verum

for V1, V2 being finite-dimensional VectSp of K

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

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

for f being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

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

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 st a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

let b2 be OrdBasis of V2; :: thesis: ( a <> 0. K implies AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) )

assume A1: a <> 0. K ; :: thesis: AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

A2: width (AutMt ((a * f),b1,b2)) = width (AutMt (f,b1,b2))

proof
end;

then A5:
width (AutMt ((a * f),b1,b2)) = width (a * (AutMt (f,b1,b2)))
by MATRIX_3:def 5;A6: len (AutMt ((a * f),b1,b2)) = len b1 by Def8

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

then A7: dom (AutMt ((a * f),b1,b2)) = dom (AutMt (f,b1,b2)) by FINSEQ_3:29;

A8: for i, j being Nat st [i,j] in Indices (AutMt ((a * f),b1,b2)) holds

(AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j)

proof

len (AutMt ((a * f),b1,b2)) = len (a * (AutMt (f,b1,b2)))
by A6, MATRIX_3:def 5;
let i, j be Nat; :: thesis: ( [i,j] in Indices (AutMt ((a * f),b1,b2)) implies (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j) )

assume A9: [i,j] in Indices (AutMt ((a * f),b1,b2)) ; :: thesis: (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j)

then A10: [i,j] in [:(dom (AutMt ((a * f),b1,b2))),(Seg (width (AutMt ((a * f),b1,b2)))):] by MATRIX_0:def 4;

then A11: [i,j] in Indices (AutMt (f,b1,b2)) by A7, A2, MATRIX_0:def 4;

(AutMt ((a * f),b1,b2)) * (i,j) = a * ((AutMt (f,b1,b2)) * (i,j))

end;assume A9: [i,j] in Indices (AutMt ((a * f),b1,b2)) ; :: thesis: (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j)

then A10: [i,j] in [:(dom (AutMt ((a * f),b1,b2))),(Seg (width (AutMt ((a * f),b1,b2)))):] by MATRIX_0:def 4;

then A11: [i,j] in Indices (AutMt (f,b1,b2)) by A7, A2, MATRIX_0:def 4;

(AutMt ((a * f),b1,b2)) * (i,j) = a * ((AutMt (f,b1,b2)) * (i,j))

proof

hence
(AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j)
by A11, MATRIX_3:def 5; :: thesis: verum
consider p2 being FinSequence of K such that

A12: p2 = (AutMt (f,b1,b2)) . i and

A13: (AutMt (f,b1,b2)) * (i,j) = p2 . j by A11, MATRIX_0:def 5;

A14: i in dom (AutMt ((a * f),b1,b2)) by A10, ZFMISC_1:87;

then A15: i in dom b1 by Lm3;

then i in dom (AutMt (f,b1,b2)) by Lm3;

then A16: p2 = (AutMt (f,b1,b2)) /. i by A12, PARTFUN1:def 6

.= (f . (b1 /. i)) |-- b2 by A15, Def8 ;

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

consider p1 being FinSequence of K such that

A17: p1 = (AutMt ((a * f),b1,b2)) . i and

A18: (AutMt ((a * f),b1,b2)) * (i,j) = p1 . j by A9, MATRIX_0:def 5;

consider KL1 being Linear_Combination of V2 such that

A19: ( (a * f) . (b1 /. i) = Sum KL1 & Carrier KL1 c= rng b2 ) and

A20: for t being Nat st 1 <= t & t <= len (((a * f) . (b1 /. i)) |-- b2) holds

(((a * f) . (b1 /. i)) |-- b2) /. t = KL1 . (b2 /. t) by Def7;

consider KL2 being Linear_Combination of V2 such that

A21: ( f . (b1 /. i) = Sum KL2 & Carrier KL2 c= rng b2 ) and

A22: for t being Nat st 1 <= t & t <= len ((f . (b1 /. i)) |-- b2) holds

((f . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t) by Def7;

( b4 is linearly-independent & (a * f) . (b1 /. i) = a * (f . (b1 /. i)) ) by Def4, VECTSP_7:def 3;

then A23: KL1 . (b2 /. j) = (a * KL2) . (b2 /. j) by A1, A19, A21, Th7

.= a * (KL2 . (b2 /. j)) by VECTSP_6:def 9 ;

A24: j in Seg (width (AutMt ((a * f),b1,b2))) by A10, ZFMISC_1:87;

then A25: 1 <= j by FINSEQ_1:1;

len b1 = len (AutMt ((a * f),b1,b2)) by Def8;

then dom b1 = dom (AutMt ((a * f),b1,b2)) by FINSEQ_3:29;

then dom b1 <> {} by A10, ZFMISC_1:87;

then Seg (len b1) <> {} by FINSEQ_1:def 3;

then len b1 > 0 ;

then A26: j in Seg (len b2) by A24, Th39;

then A27: j <= len b2 by FINSEQ_1:1;

then j <= len ((f . (b1 /. i)) |-- b2) by Def7;

then A28: p2 /. j = KL2 . (b2 /. j) by A25, A16, A22;

A29: j in dom b2 by A26, FINSEQ_1:def 3;

then j in dom ((f . (b1 /. i)) |-- b2) by Lm1;

then A30: (AutMt (f,b1,b2)) * (i,j) = p2 /. j by A13, A16, PARTFUN1:def 6;

A31: p1 = (AutMt ((a * f),b1,b2)) /. i by A17, A14, PARTFUN1:def 6

.= ((a * f) . (b1 /. i)) |-- b2 by A15, Def8 ;

then A32: j in dom p1 by A29, Lm1;

j <= len (((a * f) . (b1 /. i)) |-- b2) by A27, Def7;

then p1 /. j = KL1 . (b2 /. j) by A25, A31, A20;

hence (AutMt ((a * f),b1,b2)) * (i,j) = a * ((AutMt (f,b1,b2)) * (i,j)) by A18, A32, A30, A28, A23, PARTFUN1:def 6; :: thesis: verum

end;A12: p2 = (AutMt (f,b1,b2)) . i and

A13: (AutMt (f,b1,b2)) * (i,j) = p2 . j by A11, MATRIX_0:def 5;

A14: i in dom (AutMt ((a * f),b1,b2)) by A10, ZFMISC_1:87;

then A15: i in dom b1 by Lm3;

then i in dom (AutMt (f,b1,b2)) by Lm3;

then A16: p2 = (AutMt (f,b1,b2)) /. i by A12, PARTFUN1:def 6

.= (f . (b1 /. i)) |-- b2 by A15, Def8 ;

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

consider p1 being FinSequence of K such that

A17: p1 = (AutMt ((a * f),b1,b2)) . i and

A18: (AutMt ((a * f),b1,b2)) * (i,j) = p1 . j by A9, MATRIX_0:def 5;

consider KL1 being Linear_Combination of V2 such that

A19: ( (a * f) . (b1 /. i) = Sum KL1 & Carrier KL1 c= rng b2 ) and

A20: for t being Nat st 1 <= t & t <= len (((a * f) . (b1 /. i)) |-- b2) holds

(((a * f) . (b1 /. i)) |-- b2) /. t = KL1 . (b2 /. t) by Def7;

consider KL2 being Linear_Combination of V2 such that

A21: ( f . (b1 /. i) = Sum KL2 & Carrier KL2 c= rng b2 ) and

A22: for t being Nat st 1 <= t & t <= len ((f . (b1 /. i)) |-- b2) holds

((f . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t) by Def7;

( b4 is linearly-independent & (a * f) . (b1 /. i) = a * (f . (b1 /. i)) ) by Def4, VECTSP_7:def 3;

then A23: KL1 . (b2 /. j) = (a * KL2) . (b2 /. j) by A1, A19, A21, Th7

.= a * (KL2 . (b2 /. j)) by VECTSP_6:def 9 ;

A24: j in Seg (width (AutMt ((a * f),b1,b2))) by A10, ZFMISC_1:87;

then A25: 1 <= j by FINSEQ_1:1;

len b1 = len (AutMt ((a * f),b1,b2)) by Def8;

then dom b1 = dom (AutMt ((a * f),b1,b2)) by FINSEQ_3:29;

then dom b1 <> {} by A10, ZFMISC_1:87;

then Seg (len b1) <> {} by FINSEQ_1:def 3;

then len b1 > 0 ;

then A26: j in Seg (len b2) by A24, Th39;

then A27: j <= len b2 by FINSEQ_1:1;

then j <= len ((f . (b1 /. i)) |-- b2) by Def7;

then A28: p2 /. j = KL2 . (b2 /. j) by A25, A16, A22;

A29: j in dom b2 by A26, FINSEQ_1:def 3;

then j in dom ((f . (b1 /. i)) |-- b2) by Lm1;

then A30: (AutMt (f,b1,b2)) * (i,j) = p2 /. j by A13, A16, PARTFUN1:def 6;

A31: p1 = (AutMt ((a * f),b1,b2)) /. i by A17, A14, PARTFUN1:def 6

.= ((a * f) . (b1 /. i)) |-- b2 by A15, Def8 ;

then A32: j in dom p1 by A29, Lm1;

j <= len (((a * f) . (b1 /. i)) |-- b2) by A27, Def7;

then p1 /. j = KL1 . (b2 /. j) by A25, A31, A20;

hence (AutMt ((a * f),b1,b2)) * (i,j) = a * ((AutMt (f,b1,b2)) * (i,j)) by A18, A32, A30, A28, A23, PARTFUN1:def 6; :: thesis: verum

hence AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) by A5, A8, MATRIX_0:21; :: thesis: verum