( rng <*b*> = {b} & b in Bags I ) by PRE_POLY:def 12, FINSEQ_1:39;
hence for b₁ being FinSequence st b₁ = <*b*> holds
b₁ is Bags I -valued by RELAT_1:def 19, ZFMISC_1:31; :: thesis: verum