consider f being non empty Function;
take p = <*f*>; :: thesis: ( p is FuncSeq-like & not p is empty & p is non-empty )
thus p is FuncSeq-like ; :: thesis: ( not p is empty & p is non-empty )
thus not p is empty ; :: thesis: p is non-empty
let x be set ; :: according to FUNCT_1:def 15 :: thesis: ( not x in proj1 p or not p . x is empty )
assume x in dom p ; :: thesis: not p . x is empty
then x in {1} by FINSEQ_1:4, FINSEQ_1:55;
then x = 1 by TARSKI:def 1;
hence not p . x is empty by FINSEQ_1:57; :: thesis: verum