theorem :: COMPTRIG:59

for n being non zero Nat
for v being CRoot of n, 0 holds v = 0