let f be FinSequence of (TOP-REAL 2); :: thesis: dom (X_axis f) = dom f
len (X_axis f) = len f by GOBOARD1:def 1;
hence dom (X_axis f) = dom f by FINSEQ_3:29; :: thesis: verum