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) by XCMPLX_0:def 9 ; :: thesis: verum