let x, y be Surreal; :: thesis: (x + y) * (x + y) == ((x * x) + (y * y)) + ((x * y) + (y * x))
( x * (x + y) == (x * x) + (x * y) & y * (x + y) == (y * x) + (y * y) ) by Th67;
then A1: ( (x + y) * (x + y) == (x * (x + y)) + (y * (x + y)) & (x * (x + y)) + (y * (x + y)) == ((x * x) + (x * y)) + ((y * x) + (y * y)) ) by Th67, Th43;
((x * x) + (x * y)) + ((y * x) + (y * y)) = (x * x) + ((x * y) + ((y * x) + (y * y))) by Th37
.= (x * x) + (((x * y) + (y * x)) + (y * y)) by Th37
.= ((x * x) + (y * y)) + ((x * y) + (y * x)) by Th37 ;
hence (x + y) * (x + y) == ((x * x) + (y * y)) + ((x * y) + (y * x)) by A1, SURREALO:4; :: thesis: verum