let a be G_INTEG; :: thesis: ex c being G_INTEG st a = a * c
take 1 ; :: thesis: a = a * 1
thus a = a * 1 ; :: thesis: verum