w in free_magma_carrier X ;
then w in union (rng (disjoin ((free_magma_seq X) | NATPLUS ))) by CARD_3:def 4;
then consider Y being set such that
A1: ( w in Y & Y in rng (disjoin ((free_magma_seq X) | NATPLUS )) ) by TARSKI:def 4;
consider n being set such that
A2: ( n in dom (disjoin ((free_magma_seq X) | NATPLUS )) & Y = (disjoin ((free_magma_seq X) | NATPLUS )) . n ) by A1, FUNCT_1:def 5;
A3: n in dom ((free_magma_seq X) | NATPLUS ) by A2, CARD_3:def 3;
then n in NATPLUS by RELAT_1:86;
then reconsider n = n as natural non zero number ;
w in [:(((free_magma_seq X) | NATPLUS ) . n),{n}:] by A2, A1, A3, CARD_3:def 3;
then w `2 in {n} by MCART_1:10;
hence for b<sub>1</sub> being number st b<sub>1</sub> = w `2 holds
( not b₁ is empty & b₁ is natural ) by TARSKI:def 1; :: thesis: verum