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