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
AutMt (f,b1,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
AutMt (f,b1,b2) = {}
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 st len b1 = 0 holds
AutMt (f,b1,b2) = {}
let b2 be OrdBasis of V2; :: thesis: ( len b1 = 0 implies AutMt (f,b1,b2) = {} )
assume len b1 = 0 ; :: thesis: AutMt (f,b1,b2) = {}
then len (AutMt (f,b1,b2)) = 0 by Def8;
hence AutMt (f,b1,b2) = {} ; :: thesis: verum