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

proof

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

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

assume y in union (rng (disjoin fs)) ; :: thesis: ( y in [:[:X,[:[:X,X:],{1}:]:],{1}:] or y in [:[:[:[:X,X:],{1}:],X:],{2}:] )
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 {1,2} by A1, FINSEQ_1:2, FINSEQ_1:def 3;
then ( x = 1 or x = 2 ) by TARSKI:def 2;
hence ( y in [:[:X,[:[:X,X:],{1}:]:],{1}:] or y in [:[:[:[:X,X:],{1}:],X:],{2}:] ) by A2, A3, A5, A6, A7, CARD_3:def 3; :: thesis: verum

end;

assume A8: ( y in [:[:X,[:[:X,X:],{1}:]:],{1}:] or y in [:[:[:[:X,X:],{1}:],X:],{2}:] ) ; :: thesis: y in union (rng (disjoin fs))
( 1 in Seg 2 & 2 in Seg 2 ) by FINSEQ_1:1;
then A9: ( 1 in dom fs & 2 in dom fs ) by A1, FINSEQ_1:def 3;
then A10: ( 1 in dom (disjoin fs) & 2 in dom (disjoin fs) ) by CARD_3:def 3;
( [:[:X,[:[:X,X:],{1}:]:],{1}:] = (disjoin fs) . 1 & [:[:[:[:X,X:],{1}:],X:],{2}:] = (disjoin fs) . 2 ) by A2, A3, A9, CARD_3:def 3;
then ( [:[:X,[:[:X,X:],{1}:]:],{1}:] in rng (disjoin fs) & [:[:[:[:X,X:],{1}:],X:],{2}:] 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,3) = union (rng (disjoin fs)) by A1, CARD_3:def 4
.= [:[:X,[:[:X,X:],{1}:]:],{1}:] \/ [:[:[:[:X,X:],{1}:],X:],{2}:] by A4, XBOOLE_0:def 3 ; :: thesis: verum