now :: thesis: for x being object st x in dom <*X*> holds
not <*X*> . x is empty
let x be object ; :: thesis: ( x in dom <*X*> implies not <*X*> . x is empty )
assume x in dom <*X*> ; :: thesis: not <*X*> . x is empty
then x in Seg 1 by FINSEQ_1:89;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence not <*X*> . x is empty by FINSEQ_1:40; :: thesis: verum
end;
hence <*X*> is non-empty ; :: thesis: verum