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

[:(free_magma (X,1)),{1}:] c= free_magma_carrier X by Lm1;

hence X = {} by A16; :: thesis: verum

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

assume A16:
free_magma_carrier X = {}
; :: thesis: X = {} assume A1:
X = {}
; :: thesis: free_magma_carrier X = {}

defpred S_{1}[ Nat] means (free_magma_seq X) . $1 = {} ;

A2: for k being Nat st ( for n being Nat st n < k holds

S_{1}[n] ) holds

S_{1}[k]
_{1}[n]
from NAT_1:sch 4(A2);

for Y being set st Y in rng (disjoin ((free_magma_seq X) | NATPLUS)) holds

Y c= {}

hence free_magma_carrier X = {} by CARD_3:def 4; :: thesis: verum

end;defpred S

A2: for k being Nat st ( for n being Nat st n < k holds

S

S

proof

A12:
for n being Nat holds S
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A3: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[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;

end;S

assume A3: for n being Nat st n < k holds

S

( 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;

end;

suppose
k >= 2
; :: thesis: S_{1}[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= {}

hence S_{1}[k]
by A5, CARD_3:def 4; :: thesis: verum

end;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

then
union (rng (disjoin fs)) c= {}
by ZFMISC_1:76;
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, ZFMISC_1:90 ;

(disjoin fs) . p = [:(fs . p),{p}:] by A7, CARD_3:def 3

.= {} by A11, ZFMISC_1:90 ;

hence y c= {} by A6; :: thesis: verum

end;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, ZFMISC_1:90 ;

(disjoin fs) . p = [:(fs . p),{p}:] by A7, CARD_3:def 3

.= {} by A11, ZFMISC_1:90 ;

hence y c= {} by A6; :: thesis: verum

hence S

for Y being set st Y in rng (disjoin ((free_magma_seq X) | NATPLUS)) holds

Y c= {}

proof

then
union (rng (disjoin ((free_magma_seq X) | NATPLUS))) c= {}
by ZFMISC_1:76;
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

.= {} by ZFMISC_1:90 ;

hence Y c= {} by A13; :: thesis: verum

end;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

.= {} by ZFMISC_1:90 ;

hence Y c= {} by A13; :: thesis: verum

hence free_magma_carrier X = {} by CARD_3:def 4; :: thesis: verum

[:(free_magma (X,1)),{1}:] c= free_magma_carrier X by Lm1;

hence X = {} by A16; :: thesis: verum