let n be non zero Nat; :: thesis: #divs n = card (NatDivisors n)
reconsider z = 0 as Nat ;
set f = EXP z;
set X = NatDivisors n;
D1: #divs n = Sum ((EXP z) | (NatDivisors n)) by NAT_5:def 2;
EXP z = NAT --> 1 by ThEXP0;
hence #divs n = card (NatDivisors n) by D1, LemmaCard; :: thesis: verum