take p = <*<*0*>*>; :: thesis: ( p is Function-yielding & not p is empty & p is non-empty )
A1: ( dom p = {1} & p . 1 = <*0*> ) by FINSEQ_1:2, FINSEQ_1:38, FINSEQ_1:40;
thus p is Function-yielding :: thesis: ( not p is empty & p is non-empty )

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 p or p . x is set )
assume x in dom p ; :: thesis: p . x is set
hence p . x is set by A1, TARSKI:def 1; :: thesis: verum

end;

thus not p is empty ; :: thesis: p is non-empty
let x be set ; :: according to FUNCT_1:def 9 :: thesis: ( not x in proj1 p or not p . x is empty )
assume x in dom p ; :: thesis: not p . x is empty
hence not p . x is empty by A1, TARSKI:def 1; :: thesis: verum