let X be set ; :: thesis: ( X = {} iff free_magma_carrier X = {} )

hereby :: thesis: ( free_magma_carrier X = {} implies X = {} )

assume A1: X = {} ; :: thesis: free_magma_carrier X = {}
defpred S₁[ Nat] means (free_magma_seq X) . $1 = {} ;
A2: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A3: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
( k = 0 or k + 1 > 0 + 1 ) by XREAL_1:6;
then ( k = 0 or k >= 1 ) by NAT_1:13;
then ( k = 0 or k = 1 or k > 1 ) by XXREAL_0:1;
then A4: ( k = 0 or k = 1 or k + 1 > 1 + 1 ) by XREAL_1:6;

per cases ( k = 0 or k = 1 or k >= 2 ) by A4, NAT_1:13;

suppose k = 0 ; :: thesis: S₁[k]

hence S₁[k] by Def13; :: thesis: verum

end;

suppose k = 1 ; :: thesis: S₁[k]

hence S₁[k] by A1, Def13; :: thesis: verum

end;

suppose k >= 2 ; :: thesis: S₁[k]

then consider fs being FinSequence such that
A5: ( len fs = k - 1 & ( for p being Nat st p >= 1 & p <= k - 1 holds
fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . (k - p)):] ) & (free_magma_seq X) . k = Union (disjoin fs) ) by Def13;
for y being set st y in rng (disjoin fs) holds
y c= {}

proof

let y be set ; :: thesis: ( y in rng (disjoin fs) implies y c= {} )
assume y in rng (disjoin fs) ; :: thesis: y c= {}
then consider p being object such that
A6: ( p in dom (disjoin fs) & y = (disjoin fs) . p ) by FUNCT_1:def 3;
A7: p in dom fs by A6, CARD_3:def 3;
then A8: p in Seg (len fs) by FINSEQ_1:def 3;
reconsider p = p as Nat by A7;
A9: ( p >= 1 & p <= k - 1 ) by A5, A8, FINSEQ_1:1;
then p + 1 <= (k - 1) + 1 by XREAL_1:7;
then p < k by NAT_1:13;
then A10: (free_magma_seq X) . p = {} by A3;
A11: fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . (k - p)):] by A5, A9
.= {} by A10 ;
(disjoin fs) . p = [:(fs . p),{p}:] by A7, CARD_3:def 3
.= {} by A11 ;
hence y c= {} by A6; :: thesis: verum

end;

then union (rng (disjoin fs)) c= {} by ZFMISC_1:76;
hence S₁[k] by A5, CARD_3:def 4; :: thesis: verum

end;

end;

end;

A12: for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
for Y being set st Y in rng (disjoin ((free_magma_seq X) | NATPLUS)) holds
Y c= {}

proof

let Y be set ; :: thesis: ( Y in rng (disjoin ((free_magma_seq X) | NATPLUS)) implies Y c= {} )
assume Y in rng (disjoin ((free_magma_seq X) | NATPLUS)) ; :: thesis: Y c= {}
then consider n being object such that
A13: ( n in dom (disjoin ((free_magma_seq X) | NATPLUS)) & Y = (disjoin ((free_magma_seq X) | NATPLUS)) . n ) by FUNCT_1:def 3;
A14: n in dom ((free_magma_seq X) | NATPLUS) by A13, CARD_3:def 3;
then reconsider n = n as Nat ;
A15: n in dom ((free_magma_seq X) | NATPLUS) by A13, CARD_3:def 3;
(disjoin ((free_magma_seq X) | NATPLUS)) . n = [:(((free_magma_seq X) | NATPLUS) . n),{n}:] by A14, CARD_3:def 3
.= [:((free_magma_seq X) . n),{n}:] by A15, FUNCT_1:47
.= [:{},{n}:] by A12
.= {} ;
hence Y c= {} by A13; :: thesis: verum

end;

then union (rng (disjoin ((free_magma_seq X) | NATPLUS))) c= {} by ZFMISC_1:76;
hence free_magma_carrier X = {} by CARD_3:def 4; :: thesis: verum

end;

assume A16: free_magma_carrier X = {} ; :: thesis: X = {}
[:(free_magma (X,1)),{1}:] c= free_magma_carrier X by Lm1;
hence X = {} by A16; :: thesis: verum