let X, x, y be set ; for n, m being Nat 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 Nat; ( 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:7;
then consider fs being
FinSequence such that A4:
(
len fs = (n + m) - 1 & ( for
p being
Nat 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 Def13;
1
- 1
<= m - 1
by A3, XREAL_1:9;
then A5:
0 + n <= (m - 1) + n
by XREAL_1:7;
then fs . n =
[:((free_magma_seq X) . n),((free_magma_seq X) . ((n + m) - n)):]
by A4, A3
.=
[:((free_magma_seq X) . n),((free_magma_seq X) . m):]
;
then A6:
[x,y] in fs . n
by A1, A2, ZFMISC_1:def 2;
n in {n}
by TARSKI:def 1;
then A7:
[[x,y],n] in [:(fs . n),{n}:]
by A6, ZFMISC_1:def 2;
n in Seg (len fs)
by A4, A3, A5, FINSEQ_1:1;
then A8:
n in dom fs
by FINSEQ_1:def 3;
then A9:
(disjoin fs) . n = [:(fs . n),{n}:]
by CARD_3:def 3;
n in dom (disjoin fs)
by A8, CARD_3:def 3;
then
[:(fs . n),{n}:] in rng (disjoin fs)
by A9, FUNCT_1:3;
then
[[x,y],n] in union (rng (disjoin fs))
by A7, TARSKI:def 4;
hence
[[x,y],n] in free_magma (
X,
(n + m))
by A4, CARD_3:def 4;
verum end;