let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
factorization (s * t) = (factorization s) ^ (factorization t)
let H be Group-like associative multMagma-Family of I; :: thesis: for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
factorization (s * t) = (factorization s) ^ (factorization t)
let s, t be Element of (FreeProduct H); :: thesis: ( ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 implies factorization (s * t) = (factorization s) ^ (factorization t) )
reconsider f = uncurry (injection H) as ManySortedSet of FreeAtoms H by Lm5;
assume ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 ; :: thesis: factorization (s * t) = (factorization s) ^ (factorization t)
hence factorization (s * t) = f * ((nf s) ^ (nf t)) by Th66
.= (factorization s) ^ (factorization t) by FINSEQOP:9 ;
:: thesis: verum