now :: thesis: for x being object st x in dom <*X*> holds

not <*X*> . x is empty

hence
<*X*> is non-empty
; :: thesis: verumnot <*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;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