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;