let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H)
for k being Nat st 1 <= k & k <= len (factorization s) holds
ex i being Element of I ex g being Element of (H . i) st (factorization s) . k = [*i,g*]
let H be Group-like associative multMagma-Family of I; :: thesis: for s being Element of (FreeProduct H)
for k being Nat st 1 <= k & k <= len (factorization s) holds
ex i being Element of I ex g being Element of (H . i) st (factorization s) . k = [*i,g*]
let s be Element of (FreeProduct H); :: thesis: for k being Nat st 1 <= k & k <= len (factorization s) holds
ex i being Element of I ex g being Element of (H . i) st (factorization s) . k = [*i,g*]
let k be Nat; :: thesis: ( 1 <= k & k <= len (factorization s) implies ex i being Element of I ex g being Element of (H . i) st (factorization s) . k = [*i,g*] )
set F = uncurry (injection H);
assume ( 1 <= k & k <= len (factorization s) ) ; :: thesis: ex i being Element of I ex g being Element of (H . i) st (factorization s) . k = [*i,g*]
then A1: k in dom (factorization s) by FINSEQ_3:25;
then k in dom (nf s) by FUNCT_1:11;
then A2: (nf s) . k in rng (nf s) by FUNCT_1:3;
then consider x, y being object such that
A3: (nf s) . k = [x,y] by RELAT_1:def 1;
x in dom H by A2, A3, Th7;
then reconsider i = x as Element of I ;
reconsider g = y as Element of (H . i) by A2, A3, Th9;
take i ; :: thesis: ex g being Element of (H . i) st (factorization s) . k = [*i,g*]
take g ; :: thesis: (factorization s) . k = [*i,g*]
thus (factorization s) . k = (uncurry (injection H)) . ((nf s) . k) by A1, FUNCT_1:12
.= [*i,g*] by A3, Lm6 ; :: thesis: verum