Description: In a topological group, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010) (Revised by Mario Carneiro, 13-Aug-2015)
|- J = ( TopOpen ` G )
|- F = ( +f ` G )
|- ( G e. TopGrp -> F e. ( ( J tX J ) Cn J ) )
|- ( G e. TopGrp -> G e. TopMnd )
|- ( G e. TopMnd -> F e. ( ( J tX J ) Cn J ) )