let K be Field; 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; 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; 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; for b2 being OrdBasis of V2 st len b1 > 0 holds
width (AutMt (f,b1,b2)) = len b2
let b2 be OrdBasis of V2; ( len b1 > 0 implies width (AutMt (f,b1,b2)) = len b2 )
assume
len b1 > 0
; 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; verum