diffX2_1 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by Th58;
hence diffX2_1 o is continuous by JORDAN5A:27; :: thesis: verum