let n, m be Nat; :: thesis: for r being Real st (rfs r) . n = 0 & n <= m holds
(scf r) . m = 0
let r be Real; :: thesis: ( (rfs r) . n = 0 & n <= m implies (scf r) . m = 0 )
assume A1: ( (rfs r) . n = 0 & n <= m ) ; :: thesis: (scf r) . m = 0
thus (scf r) . m = [\((rfs r) . m)/] by Def4
.= [\0/] by A1, Th27
.= 0 ; :: thesis: verum