let D be non empty set ; :: thesis: for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) "
let G, H be Functional_Sequence of D,REAL; :: thesis: (G ") (#) (H ") = (G (#) H) "

now :: thesis: for n being Element of NAT holds ((G ") (#) (H ")) . n = ((G (#) H) ") . n

let n be Element of NAT ; :: thesis: ((G ") (#) (H ")) . n = ((G (#) H) ") . n
thus ((G ") (#) (H ")) . n = ((G ") . n) (#) ((H ") . n) by Def7
.= ((G . n) ^) (#) ((H ") . n) by Def2
.= ((G . n) ^) (#) ((H . n) ^) by Def2
.= ((G . n) (#) (H . n)) ^ by RFUNCT_1:27
.= ((G (#) H) . n) ^ by Def7
.= ((G (#) H) ") . n by Def2 ; :: thesis: verum

end;

hence (G ") (#) (H ") = (G (#) H) " by FUNCT_2:63; :: thesis: verum