Finished characteristic lemma
Wouldn't compile due to not closing lemma - fixed
Checked relation holds between functions
completed sentence