let V1, V2 be free finite-rank Z_Module; :: 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