let x, y, z be Surreal; :: thesis: z * ((x + y) * (x + y)) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x)))
( z * ((x + y) * (x + y)) == z * (((x * x) + (y * y)) + ((x * y) + (y * x))) & z * (((x * x) + (y * y)) + ((x * y) + (y * x))) == (z * ((x * x) + (y * y))) + (z * ((x * y) + (y * x))) ) by SURREALR:67, SURREALR:54, SURREALR:76;
then A1: z * ((x + y) * (x + y)) == (z * ((x * x) + (y * y))) + (z * ((x * y) + (y * x))) by SURREALO:4;
( z * ((x * x) + (y * y)) == (z * (x * x)) + (z * (y * y)) & z * ((x * y) + (y * x)) == (z * (x * y)) + (z * (y * x)) ) by SURREALR:67;
then (z * ((x * x) + (y * y))) + (z * ((x * y) + (y * x))) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x))) by SURREALR:66;
hence z * ((x + y) * (x + y)) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x))) by A1, SURREALO:4; :: thesis: verum