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 st len b1 = 0 holds
AutMt f,b1,b2 = {}
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 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 Def10;
then dom (AutMt f,b1,b2) = {} by FINSEQ_1:4, FINSEQ_1:def 3;
hence AutMt f,b1,b2 = {} by RELAT_1:64; :: thesis: verum