let f, g be Real_Sequence; :: thesis: for n being Nat holds
( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") )
let n be 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:8
.= (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