let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 st dim V1 = dim V2 holds
( not ker f is trivial iff Det (AutEqMt f,b1,b2) = 0. K )
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 st dim V1 = dim V2 holds
( not ker f is trivial iff Det (AutEqMt f,b1,b2) = 0. K )
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 st dim V1 = dim V2 holds
( not ker f is trivial iff Det (AutEqMt f,b1,b2) = 0. K )
let b2 be OrdBasis of V2; :: thesis: for f being linear-transformation of V1,V2 st dim V1 = dim V2 holds
( not ker f is trivial iff Det (AutEqMt f,b1,b2) = 0. K )
let f be linear-transformation of V1,V2; :: thesis: ( dim V1 = dim V2 implies ( not ker f is trivial iff Det (AutEqMt f,b1,b2) = 0. K ) )
assume A1: dim V1 = dim V2 ; :: thesis: ( not ker f is trivial iff Det (AutEqMt f,b1,b2) = 0. K )
set A = AutEqMt f,b1,b2;
A2: ( len b1 = dim V1 & dim V2 = len b2 & rank f = the_rank_of (AutMt f,b1,b2) ) by Th21, Th48;
then A3: ( AutEqMt f,b1,b2 = AutMt f,b1,b2 & dim V1 = (rank f) + (nullity f) ) by A1, Def2, RANKNULL:44;

hereby :: thesis: ( Det (AutEqMt f,b1,b2) = 0. K implies not ker f is trivial )

assume not ker f is trivial ; :: thesis: Det (AutEqMt f,b1,b2) = 0. K
then rank f <> dim V1 by A3, Th42;
hence Det (AutEqMt f,b1,b2) = 0. K by A2, A3, MATRIX13:83; :: thesis: verum

end;

assume Det (AutEqMt f,b1,b2) = 0. K ; :: thesis: not ker f is trivial
then dim (ker f) <> 0 by A2, A3, MATRIX13:83;
hence not ker f is trivial by Th42; :: thesis: verum