defpred S1[ Nat] means ( X = 0 or (free_magma_seq X) . X <> {} );
A1:
for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A2:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[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 A3:
(
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 A3, NAT_1:13;
suppose A4:
k >= 2
;
S1[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;
A6:
2
- 1
<= k - 1
by A4, XREAL_1:9;
then
1
in Seg (len fs)
by A5, FINSEQ_1:1;
then A7:
1
in dom fs
by FINSEQ_1:def 3;
then A8:
1
in dom (disjoin fs)
by CARD_3:def 3;
A9:
(disjoin fs) . 1
= [:(fs . 1),{1}:]
by A7, CARD_3:def 3;
A10:
fs . 1
= [:((free_magma_seq X) . 1),((free_magma_seq X) . (k - 1)):]
by A5, A6;
1
+ 1
<= (k - 1) + 1
by A4;
then
1
< k
by NAT_1:13;
then A11:
(free_magma_seq X) . 1
<> {}
by A2;
A12:
(- 1) + k < 0 + k
by XREAL_1:8;
k - 1
in NAT
by A6, INT_1:3;
then reconsider k9 =
k - 1 as
Nat ;
(free_magma_seq X) . k9 <> {}
by A12, A6, A2;
then consider x being
object such that A13:
x in [:(fs . 1),{1}:]
by A11, A10, XBOOLE_0:def 1;
[:(fs . 1),{1}:] c= union (rng (disjoin fs))
by A9, A8, FUNCT_1:3, ZFMISC_1:74;
hence
S1[
k]
by A13, A5, CARD_3:def 4;
verum end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 4(A1);
hence
not free_magma (X,n) is empty
; verum