let X be non empty set ; :: thesis: for w being Element of free_magma_carrier X holds w in [:(free_magma X,(w `2 )),{(w `2 )}:]
let w be Element of free_magma_carrier X; :: thesis: w in [:(free_magma X,(w `2 )),{(w `2 )}:]
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 A4: ((free_magma_seq X) | NATPLUS ) . n = (free_magma_seq X) . n by FUNCT_1:70;
reconsider n = n as natural number by A3;
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;
then w `2 = n by TARSKI:def 1;
hence w in [:(free_magma X,(w `2 )),{(w `2 )}:] by A4, A2, A1, A3, CARD_3:def 3; :: thesis: verum