let x, y be Surreal; :: thesis: ( not x == 0_No & not y == 0_No implies (x * y) " == (x ") * (y ") )
assume A1: ( not x == 0_No & not y == 0_No ) ; :: thesis: (x * y) " == (x ") * (y ")
then A2: ( x * (x ") == 1_No & 1_No == y * (y ") ) by Th33;
( ((x ") * (y ")) * (x * y) == (((x ") * (y ")) * y) * x & (((x ") * (y ")) * y) * x == ((x ") * ((y ") * y)) * x ) by SURREALR:54, SURREALR:69;
then ( ((x ") * (y ")) * (x * y) == (((y ") * y) * (x ")) * x & (((y ") * y) * (x ")) * x == ((y ") * y) * ((x ") * x) ) by SURREALO:4, SURREALR:69;
then ( ((x ") * (y ")) * (x * y) == ((y ") * y) * ((x ") * x) & ((y ") * y) * ((x ") * x) == ((y ") * y) * 1_No ) by A2, SURREALO:4, SURREALR:54;
then ((x ") * (y ")) * (x * y) == (y ") * y by SURREALO:4;
then ((x ") * (y ")) * (x * y) == 1_No by A2, SURREALO:4;
hence (x * y) " == (x ") * (y ") by A1, Lm3, Th41; :: thesis: verum