{(<*> D)} is FinSequenceSet of D

proof

let a be object ; :: according to FINSEQ_2:def 3 :: thesis: ( a in {(<*> D)} implies a is FinSequence of D )
thus ( a in {(<*> D)} implies a is FinSequence of D ) by TARSKI:def 1; :: thesis: verum

end;

hence not for b₁ being FinSequenceSet of D holds b₁ is empty ; :: thesis: verum