let x be object ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom <*f*> implies <*f*> . x is FinSequence )
assume x in dom <*f*> ; :: thesis: <*f*> . x is FinSequence
then x in {1} by FINSEQ_1:2, FINSEQ_1:38;
then x = 1 by TARSKI:def 1;
hence <*f*> . x is FinSequence ; :: thesis: verum