per cases ( not I is empty or I is empty ) ;

suppose not I is empty ; :: thesis: ( FreeProduct H is Group-like & not FreeProduct H is empty )

then reconsider I9 = I as non empty set ;
reconsider H9 = H as Group-like associative multMagma-Family of I9 ;

now :: thesis: ex e being Element of (FreeProduct H) st
for h being Element of (FreeProduct H) holds
( h * e = h & e * h = h & ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e ) )

set W = (FreeAtoms H) *+^+<0> ;
set R9 = ReductionRel H;
set R = EqCl (ReductionRel H);
reconsider e = 1_ (FreeProduct H) as Element of (FreeProduct H) ;
take e = e; :: thesis: for h being Element of (FreeProduct H) holds
( h * e = h & e * h = h & ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e ) )
let h be Element of (FreeProduct H); :: thesis: ( h * e = h & e * h = h & ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h ) by GROUP_1:def 4; :: thesis: ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e )
consider p being Element of ((FreeAtoms H) *+^+<0>) such that
A1: h = Class ((EqCl (ReductionRel H)),p) by EQREL_1:36;
p in the carrier of ((FreeAtoms H) *+^+<0>) ;
then p in (FreeAtoms H) * by MONOID_0:61;
then reconsider p9 = p as FinSequence of FreeAtoms H9 by FINSEQ_1:def 11;
consider q9 being FinSequence of FreeAtoms H9 such that
A2: len p9 = len q9 and
A3: for k being Nat
for i being Element of I9
for g being Element of (H9 . i) st p9 . k = [i,g] holds
(Rev q9) . k = [i,(g ")] by Th22;
q9 in (FreeAtoms H) * by FINSEQ_1:def 11;
then reconsider q = q9 as Element of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
set g = Class ((EqCl (ReductionRel H)),q);
reconsider g = Class ((EqCl (ReductionRel H)),q) as Element of (FreeProduct H) by EQREL_1:def 3;
take g = g; :: thesis: ( h * g = e & g * h = e )
A4: {} = 1_ ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
A5: ( p9 ^ q9 is Element of ((FreeAtoms H) *+^+<0>) & q9 ^ p9 is Element of ((FreeAtoms H) *+^+<0>) ) by MONOID_0:61;
( ReductionRel H reduces p9 ^ q9, {} & ReductionRel H reduces q9 ^ p9, {} ) by A2, A3, Th34;
then ( {} ,p9 ^ q9 are_convertible_wrt ReductionRel H & {} ,q9 ^ p9 are_convertible_wrt ReductionRel H ) by REWRITE1:25;
then ( [{},(p9 ^ q9)] in EqCl (ReductionRel H) & [{},(q9 ^ p9)] in EqCl (ReductionRel H) ) by A4, A5, MSUALG_6:41;
then ( p9 ^ q9 in Class ((EqCl (ReductionRel H)),{}) & q9 ^ p9 in Class ((EqCl (ReductionRel H)),{}) ) by EQREL_1:18;
then A6: ( Class ((EqCl (ReductionRel H)),(p9 ^ q9)) = Class ((EqCl (ReductionRel H)),{}) & Class ((EqCl (ReductionRel H)),(q9 ^ p9)) = Class ((EqCl (ReductionRel H)),{}) ) by A4, EQREL_1:23;
thus h * g = Class ((EqCl (ReductionRel H)),(p * q)) by A1, ALGSTR_4:def 4
.= Class ((EqCl (ReductionRel H)),(p9 ^ q9)) by MONOID_0:62
.= e by A4, A6, ALGSTR_4:49 ; :: thesis: g * h = e
thus g * h = Class ((EqCl (ReductionRel H)),(q * p)) by A1, ALGSTR_4:def 4
.= Class ((EqCl (ReductionRel H)),(q9 ^ p9)) by MONOID_0:62
.= e by A4, A6, ALGSTR_4:49 ; :: thesis: verum

end;

hence ( FreeProduct H is Group-like & not FreeProduct H is empty ) by GROUP_1:def 2; :: thesis: verum

end;

suppose I is empty ; :: thesis: ( FreeProduct H is Group-like & not FreeProduct H is empty )

then A7: the carrier of (FreeProduct H) = {(1_ (FreeProduct H))} by Th46;

now :: thesis: ex e being Element of (FreeProduct H) st
for h being Element of (FreeProduct H) holds
( h * e = h & e * h = h & ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e ) )

reconsider e = 1_ (FreeProduct H) as Element of (FreeProduct H) ;
take e = e; :: thesis: for h being Element of (FreeProduct H) holds
( h * e = h & e * h = h & ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e ) )
let h be Element of (FreeProduct H); :: thesis: ( h * e = h & e * h = h & ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h ) by GROUP_1:def 4; :: thesis: ex g being Element of (FreeProduct H) st
( h * g = e & g * h = e )
take g = e; :: thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by A7, TARSKI:def 1; :: thesis: verum

end;

hence ( FreeProduct H is Group-like & not FreeProduct H is empty ) by GROUP_1:def 2; :: thesis: verum

end;

end;