let X, x be set ; :: thesis: for n being Nat st n >= 2 & x in free_magma (X,n) holds
ex p, m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] )
let n be Nat; :: thesis: ( n >= 2 & x in free_magma (X,n) implies ex p, m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] ) )
assume A1: n >= 2 ; :: thesis: ( not x in free_magma (X,n) or ex p, m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] ) )
assume A2: x in free_magma (X,n) ; :: thesis: ex p, m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] )
consider fs being FinSequence such that
A3: len fs = n - 1 and
A4: for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . (n - p)):] and
A5: (free_magma_seq X) . n = Union (disjoin fs) by A1, Def13;
x in union (rng (disjoin fs)) by A2, A5, CARD_3:def 4;
then consider Y being set such that
A6: ( x in Y & Y in rng (disjoin fs) ) by TARSKI:def 4;
consider p being object such that
A7: ( p in dom (disjoin fs) & Y = (disjoin fs) . p ) by A6, FUNCT_1:def 3;
A8: p in dom fs by A7, CARD_3:def 3;
then reconsider p = p as Nat ;
A9: p in Seg (len fs) by A8, FINSEQ_1:def 3;
then A10: ( 1 <= p & p <= len fs ) by FINSEQ_1:1;
then A11: fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . (n - p)):] by A3, A4;
then x in [:[:((free_magma_seq X) . p),((free_magma_seq X) . (n - p)):],{p}:] by A6, A7, A8, CARD_3:def 3;
then A12: ( x `1 in [:((free_magma_seq X) . p),((free_magma_seq X) . (n - p)):] & x `2 in {p} ) by MCART_1:10;
- p >= - (n - 1) by A10, A3, XREAL_1:24;
then (- p) + n >= (- (n - 1)) + n by XREAL_1:7;
then n - p in NAT by INT_1:3;
then reconsider m = n - p as Nat ;
take p ; :: thesis: ex m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] )
take m ; :: thesis: ( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] )
thus ( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] ) by A3, A9, A6, A11, A7, A8, A12, CARD_3:def 3, FINSEQ_1:1, MCART_1:10, TARSKI:def 1; :: thesis: verum