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