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 Th34; :: 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 Lm8; :: thesis: ( transl (a,X) is continuous & (transl (a,X)) " is continuous )
thus transl (a,X) is continuous by Lm9; :: thesis: (transl (a,X)) " is continuous
(transl (a,X)) " = transl ((- a),X) by Th35;
hence (transl (a,X)) " is continuous by Lm9; :: thesis: verum