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 12;
then A3: n in dom (free_magma_seq X) by FUNCT_2:def 1;
n in NATPLUS by A1, NAT_LAT:def 6;
then A4: n in dom ((free_magma_seq X) | NATPLUS) by A3, RELAT_1:57;
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:47 ;
n in dom (disjoin ((free_magma_seq X) | NATPLUS)) by A4, CARD_3:def 3;
then [:(free_magma (X,n)),{n}:] in rng (disjoin ((free_magma_seq X) | NATPLUS)) by A5, FUNCT_1:3;
then x in union (rng (disjoin ((free_magma_seq X) | NATPLUS))) by 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