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 . n <> 0 by A1, SEQ_1:7;
A3: (f /" g) . n = (f . n) * ((g " ) . n) by SEQ_1:12
.= (f . n) * ((g . n) " ) by VALUED_1:10 ;
A4: (g /" h) . n = (g . n) * ((h " ) . n) by SEQ_1:12
.= (g . n) * ((h . n) " ) by VALUED_1:10 ;
A5: (f /" h) . n = (f . n) * ((h " ) . n) by SEQ_1:12
.= (f . n) * ((h . n) " ) by VALUED_1:10 ;
A6: ((g . n) " ) * (g . n) = (1 / (g . n)) * (g . n)
.= 1 by A2, XCMPLX_1:107 ;
((f /" g) (#) (g /" h)) . n = ((f . n) * ((g . n) " )) * ((g . n) * ((h . n) " )) by A3, A4, SEQ_1:12
.= ((((g . n) " ) * (g . n)) * (f . n)) * ((h . n) " )
.= (f /" h) . n by A5, A6 ;
hence ((f /" g) (#) (g /" h)) . n = (f /" h) . n ; :: thesis: verum

end;

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