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