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 Def8;

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_0:def 3;

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:10;

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

then A5: i in dom b1 by A3, FINSEQ_3:29;

s = (AutMt (f,b1,b2)) /. i by A3, A4, PARTFUN1:def 6

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

hence width (AutMt (f,b1,b2)) = len b2 by A2, Def7; :: thesis: verum

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 Def8;

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_0:def 3;

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:10;

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

then A5: i in dom b1 by A3, FINSEQ_3:29;

s = (AutMt (f,b1,b2)) /. i by A3, A4, PARTFUN1:def 6

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

hence width (AutMt (f,b1,b2)) = len b2 by A2, Def7; :: thesis: verum