let X, x, y be set ; for n, m being natural number st x in free_magma X,n & y in free_magma X,m holds
[[x,y],n] in free_magma X,(n + m)
let n, m be natural number ; ( x in free_magma X,n & y in free_magma X,m implies [[x,y],n] in free_magma X,(n + m) )
assume A1:
x in free_magma X,n
; ( not y in free_magma X,m or [[x,y],n] in free_magma X,(n + m) )
assume A2:
y in free_magma X,m
; [[x,y],n] in free_magma X,(n + m)
per cases
( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) )
;
suppose
(
n <> 0 &
m <> 0 )
;
[[x,y],n] in free_magma X,(n + m)then A3:
(
n >= 0 + 1 &
m >= 0 + 1 )
by NAT_1:13;
then
n + m >= 1
+ 1
by XREAL_1:9;
then consider fs being
FinSequence such that A4:
(
len fs = (n + m) - 1 & ( for
p being
natural number st
p >= 1 &
p <= (n + m) - 1 holds
fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . ((n + m) - p)):] ) &
(free_magma_seq X) . (n + m) = Union (disjoin fs) )
by Def14;
1
- 1
<= m - 1
by A3, XREAL_1:11;
then A5:
0 + n <= (m - 1) + n
by XREAL_1:9;
A6:
fs . n =
[:((free_magma_seq X) . n),((free_magma_seq X) . ((n + m) - n)):]
by A4, A3, A5
.=
[:((free_magma_seq X) . n),((free_magma_seq X) . m):]
;
A7:
[x,y] in fs . n
by A6, A1, A2, ZFMISC_1:def 2;
n in {n}
by TARSKI:def 1;
then A8:
[[x,y],n] in [:(fs . n),{n}:]
by A7, ZFMISC_1:def 2;
n in Seg (len fs)
by A4, A3, A5, FINSEQ_1:3;
then A9:
n in dom fs
by FINSEQ_1:def 3;
then A10:
(disjoin fs) . n = [:(fs . n),{n}:]
by CARD_3:def 3;
n in dom (disjoin fs)
by A9, CARD_3:def 3;
then
[:(fs . n),{n}:] in rng (disjoin fs)
by A10, FUNCT_1:12;
then
[[x,y],n] in union (rng (disjoin fs))
by A8, TARSKI:def 4;
hence
[[x,y],n] in free_magma X,
(n + m)
by A4, CARD_3:def 4;
verum end;