let p be FinSequence of X; :: thesis: p is non-empty
let x be set ; :: according to FUNCT_1:def 15 :: thesis: ( not x in dom p or not p . x is empty )
assume x in dom p ; :: thesis: not p . x is empty
then ( p . x in rng p & rng p c= X ) by FUNCT_1:def 5;
hence not p . x is empty ; :: thesis: verum