let n, m be Nat; :: thesis: for r being real number st (rfs r) . n = 0 & n <= m holds
(scf r) . m = 0
let r be real number ; :: 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 Def5
.= [\0 /] by A1, Th27
.= 0 ; :: thesis: verum