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) and
A2: len s = width (AutMt f,b1,b2) by MATRIX_1:def 4;
consider i being Nat such that
A3: i in dom (AutMt f,b1,b2) and
A4: (AutMt f,b1,b2) . i = s by A1, FINSEQ_2:11;
len (AutMt f,b1,b2) = len b1 by Def10;
then A5: i in dom b1 by A3, FINSEQ_3:31;
s = (AutMt f,b1,b2) /. i by A3, A4, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A5, Def10 ;
hence width (AutMt f,b1,b2) = len b2 by A2, Def9; :: thesis: verum