for n being Element of NAT holds (rseq (0,1,1,0)) . n = invNAT . n
proof
let n be Element of NAT ; :: thesis: (rseq (0,1,1,0)) . n = invNAT . n
(rseq (0,1,1,0)) . n = 1 / ((1 * n) + 0) by AlgDef
.= invNAT . n by MOEBIUS2:def 2 ;
hence (rseq (0,1,1,0)) . n = invNAT . n ; :: thesis: verum
end;
hence rseq (0,1,1,0) = invNAT by FUNCT_2:63; :: thesis: verum