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 object 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 3;
A3: n in dom ((free_magma_seq X) | NATPLUS) by A2, CARD_3:def 3;
then n in NATPLUS by RELAT_1:57;
then reconsider n = n as non zero Nat ;
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 zero & b₁ is natural ) by TARSKI:def 1; :: thesis: verum