let f be Sequence; :: thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f )
per cases ( f = {} or f <> {} ) ;
suppose f = {} ; :: thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f )
hence ( base- f = 0 & limit- f = dom f & len- f = dom f ) by Th15; :: thesis: verum
end;
suppose A1: f <> {} ; :: thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f )
(dom f) \ 0 = dom f ;
hence ( base- f = 0 & limit- f = dom f ) by A1, Th23; :: thesis: len- f = dom f
hence len- f = dom f by ORDINAL3:56; :: thesis: verum
end;
end;