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_{1} being number st b_{1} = w `2 holds

( not b_{1} is zero & b_{1} is natural )
by TARSKI:def 1; :: thesis: verum

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

( not b