let n be Element of NAT ; :: thesis: for f being FinSequence st len f > 0 & n > 0 holds
len (f | n) > 0
let f be FinSequence; :: thesis: ( len f > 0 & n > 0 implies len (f | n) > 0 )
assume that
A1: len f > 0 and
A2: n > 0 ; :: thesis: len (f | n) > 0

per cases ( n <= len f or n > len f ) ;

suppose n <= len f ; :: thesis: len (f | n) > 0

hence len (f | n) > 0 by FINSEQ_1:59, A2; :: thesis: verum

end;

suppose n > len f ; :: thesis: len (f | n) > 0

hence len (f | n) > 0 by FINSEQ_1:58, A1; :: thesis: verum

end;

end;