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