let X be set ; :: thesis: for w being Element of (free_magma X) st length w >= 2 holds
ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )
let w be Element of (free_magma X); :: thesis: ( length w >= 2 implies ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w ) )
assume A1: length w >= 2 ; :: thesis: ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )
then reconsider X9 = X as non empty set by Def18;
reconsider w9 = w as Element of (free_magma X9) ;
A2: w9 in [:(free_magma (X,(w9 `2))),{(w9 `2)}:] by Th25;
set n = length w;
A3: length w = w9 `2 by Def18;
consider fs being FinSequence such that
A4: len fs = (length w) - 1 and
A5: for p being Nat st p >= 1 & p <= (length w) - 1 holds
fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):] and
A6: (free_magma_seq X) . (length w) = Union (disjoin fs) by A1, Def13;
w9 `1 in (free_magma_seq X) . (length w) by A3, A2, MCART_1:10;
then w9 `1 in union (rng (disjoin fs)) by A6, CARD_3:def 4;
then consider Y being set such that
A7: ( w9 `1 in Y & Y in rng (disjoin fs) ) by TARSKI:def 4;
consider p being object such that
A8: ( p in dom (disjoin fs) & Y = (disjoin fs) . p ) by A7, FUNCT_1:def 3;
A9: p in dom fs by A8, CARD_3:def 3;
then reconsider p = p as Nat ;
A10: p in Seg (len fs) by A9, FINSEQ_1:def 3;
then A11: ( 1 <= p & p <= len fs ) by FINSEQ_1:1;
then fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):] by A4, A5;
then A12: w9 `1 in [:[:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):],{p}:] by A7, A8, A9, CARD_3:def 3;
then A13: ( (w9 `1) `1 in [:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):] & (w9 `1) `2 in {p} ) by MCART_1:10;
then A14: ( ((w9 `1) `1) `1 in (free_magma_seq X) . p & ((w9 `1) `1) `2 in (free_magma_seq X) . ((length w) - p) ) by MCART_1:10;
- p >= - ((length w) - 1) by A11, A4, XREAL_1:24;
then A15: (- p) + (length w) >= (- ((length w) - 1)) + (length w) by XREAL_1:7;
then (length w) - p in NAT by INT_1:3;
then reconsider m = (length w) - p as Nat ;
set w19 = [(((w9 `1) `1) `1),p];
set w29 = [(((w9 `1) `1) `2),m];
p in {p} by TARSKI:def 1;
then A16: [(((w9 `1) `1) `1),p] in [:(free_magma (X,p)),{p}:] by A14, ZFMISC_1:def 2;
m in {m} by TARSKI:def 1;
then A17: [(((w9 `1) `1) `2),m] in [:(free_magma (X,m)),{m}:] by A14, ZFMISC_1:def 2;
[:(free_magma (X,p)),{p}:] c= free_magma_carrier X by A11, Lm1;
then reconsider w19 = [(((w9 `1) `1) `1),p] as Element of free_magma_carrier X by A16;
[:(free_magma (X,m)),{m}:] c= free_magma_carrier X by A15, Lm1;
then reconsider w29 = [(((w9 `1) `1) `2),m] as Element of free_magma_carrier X by A17;
reconsider w1 = w19, w2 = w29 as Element of (free_magma X) ;
A18: length w1 = [(((w9 `1) `1) `1),p] `2 by Def18
.= p ;
A19: length w2 = [(((w9 `1) `1) `2),m] `2 by Def18
.= m ;
ex x, y being object st
( x in [:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):] & y in {p} & w9 `1 = [x,y] ) by A12, ZFMISC_1:def 2;
then A20: w9 `1 = [((w9 `1) `1),p] by TARSKI:def 1;
A21: ex x, y being object st
( x in (free_magma_seq X) . p & y in (free_magma_seq X) . ((length w) - p) & (w9 `1) `1 = [x,y] ) by A13, ZFMISC_1:def 2;
take w1 ; :: thesis: ex w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )
take w2 ; :: thesis: ( w = w1 * w2 & length w1 < length w & length w2 < length w )
ex x, y being object st
( x in free_magma (X,(w9 `2)) & y in {(w9 `2)} & w9 = [x,y] ) by A2, ZFMISC_1:def 2;
hence w = [[((w9 `1) `1),p],(length w)] by A20, Def18
.= [[((w9 `1) `1),(w1 `2)],((length w1) + (length w2))] by A18, A19
.= [[[(((w9 `1) `1) `1),(((w9 `1) `1) `2)],(w1 `2)],((length w1) + (length w2))] by A21
.= [[[(w1 `1),(w2 `1)],(w1 `2)],((length w1) + (length w2))]
.= w1 * w2 by Th31 ;
:: thesis: ( length w1 < length w & length w2 < length w )
p <= (length w) - 1 by A10, A4, FINSEQ_1:1;
then p + 1 <= ((length w) - 1) + 1 by XREAL_1:7;
hence length w1 < length w by A18, NAT_1:13; :: thesis: length w2 < length w
- 1 >= - p by A11, XREAL_1:24;
then (- 1) + ((length w) + 1) >= (- p) + ((length w) + 1) by XREAL_1:7;
then length w >= m + 1 ;
hence length w2 < length w by A19, NAT_1:13; :: thesis: verum