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 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 Def8;
hence dom (AutMt (f,b1,b2)) = dom b1 by FINSEQ_3:29; :: thesis: verum