let K be Field; :: 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 len b1 > 0 holds
width (AutMt f,b1,b2) = len 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 len b1 > 0 holds
width (AutMt f,b1,b2) = len b2
let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st len b1 > 0 holds
width (AutMt f,b1,b2) = len b2
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 st len b1 > 0 holds
width (AutMt f,b1,b2) = len b2
let b2 be OrdBasis of V2; :: thesis: ( len b1 > 0 implies width (AutMt f,b1,b2) = len b2 )
assume len b1 > 0 ; :: thesis: width (AutMt f,b1,b2) = len b2
then len (AutMt f,b1,b2) > 0 by Def10;
then consider s being FinSequence such that
A1: ( s in rng (AutMt f,b1,b2) & len s = width (AutMt f,b1,b2) ) by MATRIX_1:def 4;
consider i being Nat such that
A2: ( i in dom (AutMt f,b1,b2) & (AutMt f,b1,b2) . i = s ) by A1, FINSEQ_2:11;
len (AutMt f,b1,b2) = len b1 by Def10;
then A3: i in dom b1 by A2, FINSEQ_3:31;
s = (AutMt f,b1,b2) /. i by A2, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A3, Def10 ;
hence width (AutMt f,b1,b2) = len b2 by A1, Def9; :: thesis: verum