set H = <%G1,G2%>;
reconsider H = <%G1,G2%> as Group-like associative multMagma-Family of 2 ;
take FreeProduct H ; :: thesis: ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & FreeProduct H = FreeProduct H )
take H ; :: thesis: ( H = <%G1,G2%> & FreeProduct H = FreeProduct H )
thus ( H = <%G1,G2%> & FreeProduct H = FreeProduct H ) ; :: thesis: verum