let K be doubleLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f being nilpotent Function of V,V holds
( deg f = 0 iff [#] V = {(0. V)} )
let V be non empty ModuleStr over K; :: thesis: for f being nilpotent Function of V,V holds
( deg f = 0 iff [#] V = {(0. V)} )
let f be nilpotent Function of V,V; :: thesis: ( deg f = 0 iff [#] V = {(0. V)} )

hereby :: thesis: ( [#] V = {(0. V)} implies deg f = 0 )

assume A1: deg f = 0 ; :: thesis: [#] V = {(0. V)}
[#] V c= {(0. V)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] V or x in {(0. V)} )
assume A2: x in [#] V ; :: thesis: x in {(0. V)}
id V = f |^ 0 by VECTSP11:18
.= ZeroMap (V,V) by A1, Def5
.= the carrier of V --> (0. V) by GRCAT_1:def 7 ;
then x = ( the carrier of V --> (0. V)) . x by A2, FUNCT_1:18
.= 0. V by A2, FUNCOP_1:7 ;
hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum

end;

hence [#] V = {(0. V)} by ZFMISC_1:33; :: thesis: verum

end;

assume A3: [#] V = {(0. V)} ; :: thesis: deg f = 0

now :: thesis: for x being object st x in dom (f |^ 0) holds
(f |^ 0) . x = 0. V

let x be object ; :: thesis: ( x in dom (f |^ 0) implies (f |^ 0) . x = 0. V )
assume x in dom (f |^ 0) ; :: thesis: (f |^ 0) . x = 0. V
then reconsider v = x as Vector of V by FUNCT_2:def 1;
thus (f |^ 0) . x = (id V) . v by VECTSP11:18
.= 0. V by A3, TARSKI:def 1 ; :: thesis: verum

end;

then f |^ 0 = (dom (f |^ 0)) --> (0. V) by FUNCOP_1:11
.= the carrier of V --> (0. V) by FUNCT_2:def 1
.= ZeroMap (V,V) by GRCAT_1:def 7 ;
hence deg f = 0 by Def5; :: thesis: verum