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