let x1, x2, y1, y2 be Surreal; :: thesis: ( x1 == x2 & y1 == y2 implies x1 * y1 == x2 * y2 )
assume ( x1 == x2 & y1 == y2 ) ; :: thesis: x1 * y1 == x2 * y2
then ( x1 * y1 == x2 * y1 & x2 * y1 == x2 * y2 ) by SURREALR:54;
hence x1 * y1 == x2 * y2 by SURREALO:4; :: thesis: verum