let i be natural Number ; :: thesis: ex t being Nat st i = i * t
i = i * 1 ;
hence ex t being Nat st i = i * t ; :: thesis: verum