let n be Nat; :: thesis: for b, d being Real holds (rseq (0,b,0,d)) . n = b / d
let b, d be Real; :: thesis: (rseq (0,b,0,d)) . n = b / d
thus (rseq (0,b,0,d)) . n = ((0 * n) + b) / ((0 * n) + d) by Th5
.= b / d ; :: thesis: verum