let n be Nat; :: thesis: for f being n -long FinSequence st f is empty holds
n = 0
let f be n -long FinSequence; :: thesis: ( f is empty implies n = 0 )
assume f is empty ; :: thesis: n = 0
then A1: dom f = Seg 0 ;
len f = n by FINSEQ_1:def 18;
hence n = 0 by A1, FINSEQ_1:def 3; :: thesis: verum