let X be set ; :: thesis: for n being natural number st n > 0 holds
[:(free_magma X,n),{n}:] c= free_magma_carrier X
let n be natural number ; :: thesis: ( n > 0 implies [:(free_magma X,n),{n}:] c= free_magma_carrier X )
assume A1: n > 0 ; :: thesis: [:(free_magma X,n),{n}:] c= free_magma_carrier X
for x being set st x in [:(free_magma X,n),{n}:] holds
x in free_magma_carrier X

proof

let x be set ; :: thesis: ( x in [:(free_magma X,n),{n}:] implies x in free_magma_carrier X )
assume A2: x in [:(free_magma X,n),{n}:] ; :: thesis: x in free_magma_carrier X
n in NAT by ORDINAL1:def 13;
then A3: n in dom (free_magma_seq X) by FUNCT_2:def 1;
n in NATPLUS by A1, NAT_LAT:def 9;
then A4: n in dom ((free_magma_seq X) | NATPLUS ) by A3, RELAT_1:86;
then A5: (disjoin ((free_magma_seq X) | NATPLUS )) . n = [:(((free_magma_seq X) | NATPLUS ) . n),{n}:] by CARD_3:def 3
.= [:((free_magma_seq X) . n),{n}:] by A4, FUNCT_1:70 ;
n in dom (disjoin ((free_magma_seq X) | NATPLUS )) by A4, CARD_3:def 3;
then A6: [:(free_magma X,n),{n}:] in rng (disjoin ((free_magma_seq X) | NATPLUS )) by A5, FUNCT_1:12;
x in union (rng (disjoin ((free_magma_seq X) | NATPLUS ))) by A6, A2, TARSKI:def 4;
hence x in free_magma_carrier X by CARD_3:def 4; :: thesis: verum

end;

hence [:(free_magma X,n),{n}:] c= free_magma_carrier X by TARSKI:def 3; :: thesis: verum