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