set f = the Ordinal-Sequence;
take <% the Ordinal-Sequence%> ; :: thesis: ( not <% the Ordinal-Sequence%> is empty & <% the Ordinal-Sequence%> is Ordinal-Sequence-valued & <% the Ordinal-Sequence%> is with_the_same_dom )
thus ( not <% the Ordinal-Sequence%> is empty & <% the Ordinal-Sequence%> is Ordinal-Sequence-valued & <% the Ordinal-Sequence%> is with_the_same_dom ) ; :: thesis: verum