let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for k being Nat
for s being Element of (FreeProduct H) st k <= len (nf s) holds
ex s1, s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
let H be Group-like associative multMagma-Family of I; :: thesis: for k being Nat
for s being Element of (FreeProduct H) st k <= len (nf s) holds
ex s1, s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
let k be Nat; :: thesis: for s being Element of (FreeProduct H) st k <= len (nf s) holds
ex s1, s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
let s be Element of (FreeProduct H); :: thesis: ( k <= len (nf s) implies ex s1, s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k ) )
assume A1: k <= len (nf s) ; :: thesis: ex s1, s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
set s1 = Class ((EqCl (ReductionRel H)),((nf s) | k));
(nf s) | k in (FreeAtoms H) * by FINSEQ_1:def 11;
then (nf s) | k is Element of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
then reconsider s1 = Class ((EqCl (ReductionRel H)),((nf s) | k)) as Element of (FreeProduct H) by EQREL_1:def 3;
set s2 = Class ((EqCl (ReductionRel H)),((nf s) /^ k));
(nf s) /^ k in (FreeAtoms H) * by FINSEQ_1:def 11;
then (nf s) /^ k is Element of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
then reconsider s2 = Class ((EqCl (ReductionRel H)),((nf s) /^ k)) as Element of (FreeProduct H) by EQREL_1:def 3;
take s1 ; :: thesis: ex s2 being Element of (FreeProduct H) st
( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
take s2 ; :: thesis: ( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
consider y being Element of ((FreeAtoms H) *+^+<0>) such that
A2: s = Class ((EqCl (ReductionRel H)),y) by EQREL_1:36;
nf s in s by Def7;
hence s = Class ((EqCl (ReductionRel H)),(nf s)) by A2, EQREL_1:23
.= Class ((EqCl (ReductionRel H)),(((nf s) | k) ^ ((nf s) /^ k))) by RFINSEQ:8
.= s1 * s2 by Th47 ;
:: thesis: ( nf s = (nf s1) ^ (nf s2) & len (nf s1) = k )
thus nf s = ((nf s) | k) ^ ((nf s) /^ k) by RFINSEQ:8
.= (nf s1) ^ ((nf s) /^ k) by Th60
.= (nf s1) ^ (nf s2) by Th61 ; :: thesis: len (nf s1) = k
nf s1 = (nf s) | k by Th60;
hence len (nf s1) = k by A1, FINSEQ_1:59; :: thesis: verum