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 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 A4: ((free_magma_seq X) | NATPLUS) . n = (free_magma_seq X) . n by FUNCT_1:47;
reconsider n = n as Nat 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