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 Def19;
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 Def19;
consider fs being FinSequence such that
A4: len fs = (length w) - 1 and
A5: for p being natural number 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, Def14;
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 set such that
A8: ( p in dom (disjoin fs) & Y = (disjoin fs) . p ) by A7, FUNCT_1:def 5;
A9: p in dom fs by A8, CARD_3:def 3;
then reconsider p = p as natural number ;
A10: p in Seg (len fs) by A9, FINSEQ_1:def 3;
then A11: ( 1 <= p & p <= len fs ) by FINSEQ_1:3;
then A12: fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):] by A4, A5;
A13: w9 `1 in [:[:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):],{p}:] by A7, A12, A8, A9, CARD_3:def 3;
then A14: ( (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 A15: ( ((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:26;
then A16: (- p) + (length w) >= (- ((length w) - 1)) + (length w) by XREAL_1:9;
then (length w) - p in NAT by INT_1:16;
then reconsider m = (length w) - p as natural number ;
set w19 = [(((w9 `1 ) `1 ) `1 ),p];
set w29 = [(((w9 `1 ) `1 ) `2 ),m];
p in {p} by TARSKI:def 1;
then A17: [(((w9 `1 ) `1 ) `1 ),p] in [:(free_magma X,p),{p}:] by A15, ZFMISC_1:def 2;
m in {m} by TARSKI:def 1;
then A18: [(((w9 `1 ) `1 ) `2 ),m] in [:(free_magma X,m),{m}:] by A15, 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 A17;
[:(free_magma X,m),{m}:] c= free_magma_carrier X by A16, Lm1;
then reconsider w29 = [(((w9 `1 ) `1 ) `2 ),m] as Element of free_magma_carrier X by A18;
reconsider w1 = w19, w2 = w29 as Element of (free_magma X) ;
A19: length w1 = w19 `2 by Def19
.= p by MCART_1:def 2 ;
A20: length w2 = w29 `2 by Def19
.= m by MCART_1:def 2 ;
ex x, y being set st
( x in [:((free_magma_seq X) . p),((free_magma_seq X) . ((length w) - p)):] & y in {p} & w9 `1 = [x,y] ) by A13, ZFMISC_1:def 2;
then A21: w9 `1 = [((w9 `1 ) `1 ),((w9 `1 ) `2 )] by MCART_1:8
.= [((w9 `1 ) `1 ),p] by A14, TARSKI:def 1 ;
A22: ex x, y being set st
( x in (free_magma_seq X) . p & y in (free_magma_seq X) . ((length w) - p) & (w9 `1 ) `1 = [x,y] ) by A14, 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 )
A23: ex x, y being set st
( x in free_magma X,(w9 `2 ) & y in {(w9 `2 )} & w9 = [x,y] ) by A2, ZFMISC_1:def 2;
thus w = [(w9 `1 ),(w9 `2 )] by A23, MCART_1:8
.= [[((w9 `1 ) `1 ),p],(length w)] by A21, Def19
.= [[((w9 `1 ) `1 ),(w1 `2 )],((length w1) + (length w2))] by A19, A20, MCART_1:def 2
.= [[[(((w9 `1 ) `1 ) `1 ),(((w9 `1 ) `1 ) `2 )],(w1 `2 )],((length w1) + (length w2))] by A22, MCART_1:8
.= [[[(((w9 `1 ) `1 ) `1 ),(w2 `1 )],(w1 `2 )],((length w1) + (length w2))] by MCART_1:def 1
.= [[[(w1 `1 ),(w2 `1 )],(w1 `2 )],((length w1) + (length w2))] by MCART_1:def 1
.= w1 * w2 by Th31 ; :: thesis: ( length w1 < length w & length w2 < length w )
p <= (length w) - 1 by A10, FINSEQ_1:3, A4;
then p + 1 <= ((length w) - 1) + 1 by XREAL_1:9;
hence length w1 < length w by A19, NAT_1:13; :: thesis: length w2 < length w
- 1 >= - p by A11, XREAL_1:26;
then (- 1) + ((length w) + 1) >= (- p) + ((length w) + 1) by XREAL_1:9;
then length w >= m + 1 ;
hence length w2 < length w by A20, NAT_1:13; :: thesis: verum