let n be Nat; :: thesis: (rseq (0,1,1,0)) . n = 1 / n
thus (rseq (0,1,1,0)) . n = ((0 * n) + 1) / ((1 * n) + 0) by Th5
.= 1 / n ; :: thesis: verum