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

let n be Element of NAT ; :: thesis: ((G " ) (#) (H " )) . n = ((G (#) H) " ) . n
thus ((G " ) (#) (H " )) . n = ((G " ) . n) (#) ((H " ) . n) by Def8
.= ((G . n) ^ ) (#) ((H " ) . n) by Def3
.= ((G . n) ^ ) (#) ((H . n) ^ ) by Def3
.= ((G . n) (#) (H . n)) ^ by RFUNCT_1:43
.= ((G (#) H) . n) ^ by Def8
.= ((G (#) H) " ) . n by Def3 ; :: thesis: verum

end;

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