let X be set ; 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 ;
( y in union (rng (disjoin fs)) iff ( y in [:[:X,[:[:X,X:],{1}:]:],{1}:] or y in [:[:[:[:X,X:],{1}:],X:],{2}:] ) )
hereby ( ( 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))
;
( 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;
verum
end;
assume A8:
(
y in [:[:X,[:[:X,X:],{1}:]:],{1}:] or
y in [:[:[:[:X,X:],{1}:],X:],{2}:] )
;
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;
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
; verum