let D be non empty set ; :: thesis: for f being non empty XFinSequence of holds len f > 0
let f be non empty XFinSequence of ; :: thesis: len f > 0
len f <> 0 by AFINSQ_1:18;
hence len f > 0 ; :: thesis: verum