let a be Integer; :: thesis: ex i3 being Integer st a = a * i3
take 1 ; :: thesis: a = a * 1
thus a = a * 1 ; :: thesis: verum