let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I st I is trivial holds
H . i, FreeProduct H are_isomorphic
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I st I is trivial holds
H . i, FreeProduct H are_isomorphic
let H be Group-like associative multMagma-Family of I; :: thesis: ( I is trivial implies H . i, FreeProduct H are_isomorphic )
assume I is trivial ; :: thesis: H . i, FreeProduct H are_isomorphic
then injection (H,i) is bijective by Th57;
hence H . i, FreeProduct H are_isomorphic by GROUP_6:def 11; :: thesis: verum