let f be FinSequence of ; :: thesis: dom (Y_axis f) = dom f
len (Y_axis f) = len f by GOBOARD1:def 4;
hence dom (Y_axis f) = dom f by FINSEQ_3:31; :: thesis: verum