let p be FinSequence; :: thesis: for k being set st k in dom p holds
len p > 0
let k be set ; :: thesis: ( k in dom p implies len p > 0 )
assume k in dom p ; :: thesis: len p > 0
then p <> {} by RELAT_1:60;
then len p <> 0 ;
hence len p > 0 ; :: thesis: verum