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 holds dom (AutMt f,b1,b2) = dom b1
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 holds dom (AutMt f,b1,b2) = dom b1
let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds dom (AutMt f,b1,b2) = dom b1
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 holds dom (AutMt f,b1,b2) = dom b1
let b2 be OrdBasis of V2; :: thesis: dom (AutMt f,b1,b2) = dom b1
len (AutMt f,b1,b2) = len b1 by Def10;
hence dom (AutMt f,b1,b2) = dom b1 by FINSEQ_3:31; :: thesis: verum