take FreeProduct ( the Cardinal --> INT.Group) ; :: thesis: FreeProduct ( the Cardinal --> INT.Group) is free
thus FreeProduct ( the Cardinal --> INT.Group) is free ; :: thesis: verum