let x, y, z be Surreal; ((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == (x - (y * y)) * (x - (z * z))
( (y * z) * (y * z) == z * (y * (y * z)) & z * (y * (y * z)) == z * ((y * y) * z) )
by SURREALR:54, SURREALR:69;
then
( (y * z) * (y * z) == (z * (y * y)) * z & (z * (y * y)) * z == (z * z) * (y * y) )
by SURREALO:4, SURREALR:69;
then
(y * z) * (y * z) == (z * z) * (y * y)
by SURREALO:4;
then
(x * x) + ((y * z) * (y * z)) == (x * x) + ((z * z) * (y * y))
by SURREALR:66;
then A1:
((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == ((x * x) + ((z * z) * (y * y))) - ((x * (y * y)) + (x * (z * z)))
by SURREALR:66;
( x * (x - (z * z)) == (x * x) + (x * (- (z * z))) & (- (y * y)) * (x - (z * z)) == ((- (y * y)) * x) + ((- (y * y)) * (- (z * z))) )
by SURREALR:67;
then
( (x + (- (y * y))) * (x - (z * z)) == (x * (x - (z * z))) + ((- (y * y)) * (x - (z * z))) & (x * (x - (z * z))) + ((- (y * y)) * (x - (z * z))) == ((x * x) + (x * (- (z * z)))) + (((- (y * y)) * x) + ((- (y * y)) * (- (z * z)))) )
by SURREALR:67, SURREALR:66;
then A2:
(x + (- (y * y))) * (x - (z * z)) == ((x * x) + (x * (- (z * z)))) + (((- (y * y)) * x) + ((- (y * y)) * (- (z * z))))
by SURREALO:4;
( (- (y * y)) * (- (z * z)) = (y * y) * (z * z) & x * (- (z * z)) = - (x * (z * z)) & (- (y * y)) * x = - (x * (y * y)) )
by SURREALR:58;
then ((x * x) + (x * (- (z * z)))) + (((- (y * y)) * x) + ((- (y * y)) * (- (z * z)))) =
(((x * x) + (- (x * (z * z)))) + (- ((y * y) * x))) + ((y * y) * (z * z))
by SURREALR:37
.=
((x * x) + ((- (x * (z * z))) + (- ((y * y) * x)))) + ((y * y) * (z * z))
by SURREALR:37
.=
((x * x) + ((y * y) * (z * z))) + ((- (x * (z * z))) + (- ((y * y) * x)))
by SURREALR:37
.=
((x * x) + ((y * y) * (z * z))) + (- ((x * (z * z)) + ((y * y) * x)))
by SURREALR:40
;
hence
((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == (x - (y * y)) * (x - (z * z))
by A2, A1, SURREALO:4; verum