take 1_ G ; :: thesis: 1_ G is m -power
thus 1_ G is m -power by Th13; :: thesis: verum