thus dom (transl a,X) = [#] X by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng (transl a,X) = [#] X & transl a,X is one-to-one & transl a,X is continuous & (transl a,X) " is continuous )
thus rng (transl a,X) = [#] X by Th35; :: thesis: ( transl a,X is one-to-one & transl a,X is continuous & (transl a,X) " is continuous )
thus transl a,X is one-to-one by Lm9; :: thesis: ( transl a,X is continuous & (transl a,X) " is continuous )
thus transl a,X is continuous by Lm10; :: thesis: (transl a,X) " is continuous
(transl a,X) " = transl (- a),X by Th36;
hence (transl a,X) " is continuous by Lm10; :: thesis: verum