let f, g, h be Real_Sequence; :: thesis: ( g is non-zero implies (f /" g) (#) (g /" h) = f /" h )
set f3 = f /" g;
set g3 = g /" h;
set h3 = f /" h;
assume A1: g is non-zero ; :: thesis: (f /" g) (#) (g /" h) = f /" h
for n being Element of NAT holds ((f /" g) (#) (g /" h)) . n = (f /" h) . n

proof

let n be Element of NAT ; :: thesis: ((f /" g) (#) (g /" h)) . n = (f /" h) . n
set a = f . n;
set b = (g . n) " ;
set c = g . n;
set d = (h . n) " ;
A2: (g /" h) . n = (g . n) * ((h ") . n) by SEQ_1:8
.= (g . n) * ((h . n) ") by VALUED_1:10 ;
A3: (f /" h) . n = (f . n) * ((h ") . n) by SEQ_1:8
.= (f . n) * ((h . n) ") by VALUED_1:10 ;
A4: g . n <> 0 by A1, SEQ_1:5;
A5: ((g . n) ") * (g . n) = (1 / (g . n)) * (g . n)
.= 1 by A4, XCMPLX_1:106 ;
(f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8
.= (f . n) * ((g . n) ") by VALUED_1:10 ;
then ((f /" g) (#) (g /" h)) . n = ((f . n) * ((g . n) ")) * ((g . n) * ((h . n) ")) by A2, SEQ_1:8
.= ((((g . n) ") * (g . n)) * (f . n)) * ((h . n) ")
.= (f /" h) . n by A3, A5 ;
hence ((f /" g) (#) (g /" h)) . n = (f /" h) . n ; :: thesis: verum

end;

hence (f /" g) (#) (g /" h) = f /" h by FUNCT_2:63; :: thesis: verum