diffX2_2 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by Th59;
hence diffX2_2 o is continuous by TOPREAL6:83; :: thesis: verum