let x be Surreal; :: thesis: x * 0_No = 0_No
A1: ( comp ((L_ x),x,0_No,(L_ 0_No)) = {} & comp ((R_ x),x,0_No,(R_ 0_No)) = {} ) by Th49;
x * 0_No = [((comp ((L_ x),x,0_No,(L_ 0_No))) \/ (comp ((R_ x),x,0_No,(R_ 0_No)))),((comp ((L_ x),x,0_No,(L_ 0_No))) \/ (comp ((R_ x),x,0_No,(L_ 0_No))))] by Th50;
hence x * 0_No = 0_No by A1; :: thesis: verum