let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) holds Product (factorization s) = s
let H be Group-like associative multMagma-Family of I; :: thesis: for s being Element of (FreeProduct H) holds Product (factorization s) = s
let s be Element of (FreeProduct H); :: thesis: Product (factorization s) = s
defpred S₁[ Nat] means for s being Element of (FreeProduct H) st len (nf s) = $1 holds
Product (factorization s) = s;
A1: S₁[ 0 ]

proof

let s be Element of (FreeProduct H); :: thesis: ( len (nf s) = 0 implies Product (factorization s) = s )
assume len (nf s) = 0 ; :: thesis: Product (factorization s) = s
then A2: s = 1_ (FreeProduct H) by Th63;
hence Product (factorization s) = Product (<*> the carrier of (FreeProduct H)) by Th68
.= s by A2, GROUP_4:8 ;
:: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let s be Element of (FreeProduct H); :: thesis: ( len (nf s) = k + 1 implies Product (factorization s) = s )
assume A5: len (nf s) = k + 1 ; :: thesis: Product (factorization s) = s
then k + 0 <= len (nf s) by XREAL_1:6;
then consider s1, s2 being Element of (FreeProduct H) such that
A6: ( s = s1 * s2 & nf s = (nf s1) ^ (nf s2) & len (nf s1) = k ) by Th67;
len (nf s) = (len (nf s1)) + (len (nf s2)) by A6, FINSEQ_1:22;
then A7: 1 = len (nf s2) by A5, A6;
then consider i being Element of I, g being Element of (H . i) such that
A8: ( g <> 1_ (H . i) & s2 = [*i,g*] ) by Th65;
reconsider r = <*s2*> as FinSequence of (FreeProduct H) ;

per cases ( len (nf s1) <> 0 or len (nf s1) = 0 ) ;

suppose len (nf s1) <> 0 ; :: thesis: Product (factorization s) = s

then A9: ((nf s1) . (len (nf s1))) `1 <> ((nf s2) . 1) `1 by A6, A7, Def7, Th44;
thus Product (factorization s) = Product ((factorization s1) ^ (factorization s2)) by A6, A9, Th70
.= (Product (factorization s1)) * (Product (factorization s2)) by GROUP_4:5
.= s1 * (Product (factorization s2)) by A4, A6
.= s1 * (Product r) by A8, Th69
.= s by A6, GROUP_4:9 ; :: thesis: verum

end;

suppose len (nf s1) = 0 ; :: thesis: Product (factorization s) = s

then A10: s1 = 1_ (FreeProduct H) by Th63;
thus Product (factorization s) = Product (factorization s2) by A6, A10, GROUP_1:def 4
.= Product r by A8, Th69
.= s2 by GROUP_4:9
.= s by A6, A10, GROUP_1:def 4 ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
then S₁[ len (nf s)] ;
hence Product (factorization s) = s ; :: thesis: verum