let X be set ; :: thesis: free_magma (X,2) = [:[:X,X:],{1}:]
consider fs being FinSequence such that
A1: ( len fs = 2 - 1 & ( for p being Nat st p >= 1 & p <= 2 - 1 holds
fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . (2 - p)):] ) & (free_magma_seq X) . 2 = Union (disjoin fs) ) by Def13;
A2: fs . 1 = [:((free_magma_seq X) . 1),((free_magma_seq X) . (2 - 1)):] by A1
.= [:(free_magma (X,1)),X:] by Def13
.= [:X,X:] by Def13 ;
then A3: fs = <*[:X,X:]*> by A1, FINSEQ_1:40;
A4: for y being object holds
( y in union (rng (disjoin fs)) iff y in [:[:X,X:],{1}:] )

proof

let y be object ; :: thesis: ( y in union (rng (disjoin fs)) iff y in [:[:X,X:],{1}:] )

hereby :: thesis: ( y in [:[:X,X:],{1}:] implies y in union (rng (disjoin fs)) )

assume y in union (rng (disjoin fs)) ; :: thesis: y in [:[:X,X:],{1}:]
then consider Y being set such that
A5: ( y in Y & Y in rng (disjoin fs) ) by TARSKI:def 4;
consider x being object such that
A6: ( x in dom (disjoin fs) & Y = (disjoin fs) . x ) by A5, FUNCT_1:def 3;
A7: x in dom fs by A6, CARD_3:def 3;
then x in Seg 1 by A3, FINSEQ_1:38;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence y in [:[:X,X:],{1}:] by A5, A2, A6, A7, CARD_3:def 3; :: thesis: verum

end;

assume A8: y in [:[:X,X:],{1}:] ; :: thesis: y in union (rng (disjoin fs))
1 in Seg 1 by FINSEQ_1:1;
then A9: 1 in dom fs by A3, FINSEQ_1:38;
then A10: 1 in dom (disjoin fs) by CARD_3:def 3;
[:[:X,X:],{1}:] = (disjoin fs) . 1 by A2, A9, CARD_3:def 3;
then [:[:X,X:],{1}:] in rng (disjoin fs) by A10, FUNCT_1:def 3;
hence y in union (rng (disjoin fs)) by A8, TARSKI:def 4; :: thesis: verum

end;

thus free_magma (X,2) = union (rng (disjoin fs)) by A1, CARD_3:def 4
.= [:[:X,X:],{1}:] by A4, TARSKI:2 ; :: thesis: verum