Moebius 1 = (- 1) |^ (card 0) by Def3, Th7, Th22
.= 1 by NEWTON:4 ;
hence Moebius 1 = 1 ; :: thesis: verum