let f be FinSequence of (TOP-REAL 2); :: thesis: ( f <> {} implies X_axis f <> {} )
A1: len (X_axis f) = len f by GOBOARD1:def 1;
assume ( f <> {} & X_axis f = {} ) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum