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: len (AutMt (a * f),b1,b2) = len b1 by Def10
.= len (AutMt f,b1,b2) by Def10 ;
then A3: len (AutMt (a * f),b1,b2) = len (a * (AutMt f,b1,b2)) by MATRIX_3:def 5;
A4: dom (AutMt (a * f),b1,b2) = dom (AutMt f,b1,b2) by A2, FINSEQ_3:31;
A5: width (AutMt (a * f),b1,b2) = width (AutMt f,b1,b2)

proof

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

suppose A6: len b1 = 0 ; :: thesis: width (AutMt (a * f),b1,b2) = width (AutMt f,b1,b2)

then AutMt (a * f),b1,b2 = {} by Th43
.= AutMt f,b1,b2 by A6, Th43 ;
hence width (AutMt (a * f),b1,b2) = width (AutMt f,b1,b2) ; :: thesis: verum

end;

suppose A7: len b1 > 0 ; :: thesis: width (AutMt (a * f),b1,b2) = width (AutMt f,b1,b2)

hence width (AutMt (a * f),b1,b2) = len b2 by Th44
.= width (AutMt f,b1,b2) by A7, Th44 ;
:: thesis: verum

end;

end;

end;

then A8: width (AutMt (a * f),b1,b2) = width (a * (AutMt f,b1,b2)) by MATRIX_3:def 5;
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

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_1:def 5;
then A11: [i,j] in Indices (AutMt f,b1,b2) by A4, A5, MATRIX_1:def 5;
(AutMt (a * f),b1,b2) * i,j = a * ((AutMt f,b1,b2) * i,j)

proof

consider p1 being FinSequence of K such that
A12: ( p1 = (AutMt (a * f),b1,b2) . i & (AutMt (a * f),b1,b2) * i,j = p1 . j ) by A9, MATRIX_1:def 6;
consider p2 being FinSequence of K such that
A13: ( p2 = (AutMt f,b1,b2) . i & (AutMt f,b1,b2) * i,j = p2 . j ) by A11, MATRIX_1:def 6;
A14: j in Seg (width (AutMt (a * f),b1,b2)) by A10, ZFMISC_1:106;
len b1 = len (AutMt (a * f),b1,b2) by Def10;
then dom b1 = dom (AutMt (a * f),b1,b2) by FINSEQ_3:31;
then dom b1 <> {} by A10, ZFMISC_1:106;
then Seg (len b1) <> {} by FINSEQ_1:def 3;
then A15: j in Seg (len b2) by A14, Th44, FINSEQ_1:4, NAT_1:3;
then A16: ( 1 <= j & j <= len b2 ) by FINSEQ_1:3;
A17: j in dom b2 by A15, FINSEQ_1:def 3;
A18: i in dom (AutMt (a * f),b1,b2) by A10, ZFMISC_1:106;
then A19: i in dom b1 by Lm3;
then A20: i in dom (AutMt f,b1,b2) by Lm3;
A21: ( 1 <= j & j <= len (((a * f) . (b1 /. i)) |-- b2) ) by A16, Def9;
A22: ( 1 <= j & j <= len ((f . (b1 /. i)) |-- b2) ) by A16, Def9;
A23: p1 = (AutMt (a * f),b1,b2) /. i by A12, A18, PARTFUN1:def 8
.= ((a * f) . (b1 /. i)) |-- b2 by A19, Def10 ;
A24: p2 = (AutMt f,b1,b2) /. i by A13, A20, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A19, Def10 ;
A25: j in dom p1 by A17, A23, Lm1;
j in dom ((f . (b1 /. i)) |-- b2) by A17, Lm1;
then A26: (AutMt f,b1,b2) * i,j = p2 /. j by A13, A24, PARTFUN1:def 8;
consider KL1 being Linear_Combination of V2 such that
A27: ( (a * f) . (b1 /. i) = Sum KL1 & Carrier KL1 c= rng b2 & ( 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 Def9;
consider KL2 being Linear_Combination of V2 such that
A28: ( f . (b1 /. i) = Sum KL2 & Carrier KL2 c= rng b2 & ( for t being Nat st 1 <= t & t <= len ((f . (b1 /. i)) |-- b2) holds
((f . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t) ) ) by Def9;
A29: p1 /. j = KL1 . (b2 /. j) by A21, A23, A27;
A30: p2 /. j = KL2 . (b2 /. j) by A22, A24, A28;
reconsider b4 = rng b2 as Basis of V2 by Def4;
A31: b4 is linearly-independent by VECTSP_7:def 3;
(a * f) . (b1 /. i) = a * (f . (b1 /. i)) by Def6;
then KL1 . (b2 /. j) = (a * KL2) . (b2 /. j) by A1, A27, A28, A31, Th11
.= a * (KL2 . (b2 /. j)) by VECTSP_6:def 12 ;
hence (AutMt (a * f),b1,b2) * i,j = a * ((AutMt f,b1,b2) * i,j) by A12, A25, A26, A29, A30, PARTFUN1:def 8; :: thesis: verum

end;

hence (AutMt (a * f),b1,b2) * i,j = (a * (AutMt f,b1,b2)) * i,j by A11, MATRIX_3:def 5; :: thesis: verum

end;

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