let x be set ; :: according to REWRITE2:def 1 :: thesis: ( x in dom <*f*> implies <*f*> . x is XFinSequence )

assume x in dom <*f*> ; :: thesis: <*f*> . x is XFinSequence

then x in {1} by FINSEQ_1:2, FINSEQ_1:38;

then x = 1 by TARSKI:def 1;

hence <*f*> . x is XFinSequence by FINSEQ_1:40; :: thesis: verum

assume x in dom <*f*> ; :: thesis: <*f*> . x is XFinSequence

then x in {1} by FINSEQ_1:2, FINSEQ_1:38;

then x = 1 by TARSKI:def 1;

hence <*f*> . x is XFinSequence by FINSEQ_1:40; :: thesis: verum