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;
thus p is Function-yielding ; :: thesis: ( not p is empty & p is non-empty )
thus not p is empty ; :: thesis: p is non-empty
let x be object ; :: 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