let f, g be Real_Sequence; :: thesis: for n being Nat holds (f /" g) . n = (f . n) / (g . n)
let n be Nat; :: thesis: (f /" g) . n = (f . n) / (g . n)
thus (f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8
.= (f . n) * ((g . n) ") by VALUED_1:10
.= (f . n) / (g . n) ; :: thesis: verum