let I be empty set ; :: thesis: for H being Group-like associative multMagma-Family of I holds the carrier of (FreeProduct H) = {(1_ (FreeProduct H))}
let H be Group-like associative multMagma-Family of I; :: thesis: the carrier of (FreeProduct H) = {(1_ (FreeProduct H))}

now :: thesis: for x being object holds
( ( x in the carrier of (FreeProduct H) implies x = 1_ (FreeProduct H) ) & ( x = 1_ (FreeProduct H) implies x in the carrier of (FreeProduct H) ) )

let x be object ; :: thesis: ( ( x in the carrier of (FreeProduct H) implies x = 1_ (FreeProduct H) ) & ( x = 1_ (FreeProduct H) implies x in the carrier of (FreeProduct H) ) )

hereby :: thesis: ( x = 1_ (FreeProduct H) implies x in the carrier of (FreeProduct H) )

assume x in the carrier of (FreeProduct H) ; :: thesis: x = 1_ (FreeProduct H)
then A1: x in Class (EqCl (ReductionRel H)) ;
reconsider X = x as set by TARSKI:1;
consider y being object such that
A2: ( y in the carrier of ((FreeAtoms H) *+^+<0>) & X = Class ((EqCl (ReductionRel H)),y) ) by A1, EQREL_1:def 3;
y in (FreeAtoms H) * by A2, MONOID_0:61;
then y in {{}} by FUNCT_7:17;
then y = {} by TARSKI:def 1;
hence x = 1_ (FreeProduct H) by A2, Th45; :: thesis: verum

end;

assume x = 1_ (FreeProduct H) ; :: thesis: x in the carrier of (FreeProduct H)
hence x in the carrier of (FreeProduct H) ; :: thesis: verum

end;

hence the carrier of (FreeProduct H) = {(1_ (FreeProduct H))} by TARSKI:def 1; :: thesis: verum