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);
dim V2 = len b2 by Th21;
then A2: AutEqMt (f,b1,b2) = AutMt (f,b1,b2) by A1, Def2, Th21;
A3: dim V1 = (rank f) + (nullity f) by RANKNULL:44;
A4: ( len b1 = dim V1 & rank f = the_rank_of (AutMt (f,b1,b2)) ) by Th21, Th48;

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 A4, A2, 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 A4, A2, A3, MATRIX13:83;
hence not ker f is trivial by Th42; :: thesis: verum