let x, y be Surreal; :: thesis: for x1, y1, Ix1 being Surreal st x1 * Ix1 == 1_No holds
((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1)))
let x1, y1, Ix1 be Surreal; :: thesis: ( x1 * Ix1 == 1_No implies ((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1))) )
assume A1: x1 * Ix1 == 1_No ; :: thesis: ((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1)))
( x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1) == (1_No + ((x1 + (- x)) * y1)) * (x1 * Ix1) & (1_No + ((x1 + (- x)) * y1)) * (x1 * Ix1) == (1_No + ((x1 + (- x)) * y1)) * 1_No & (1_No + ((x1 + (- x)) * y1)) * 1_No = 1_No + ((x1 + (- x)) * y1) ) by A1, SURREALR:69, SURREALR:51;
then x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1) == 1_No + ((x1 + (- x)) * y1) by SURREALO:4;
then A2: ( - (x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1)) == - (1_No + ((x1 + (- x)) * y1)) & - (1_No + ((x1 + (- x)) * y1)) = (- 1_No) + (- ((x1 + (- x)) * y1)) ) by SURREALR:10, SURREALR:40;
- ((x1 + (- x)) * y1) == - ((x1 * y1) + ((- x) * y1)) by SURREALR:65, SURREALR:67;
then (- 1_No) + (- ((x1 + (- x)) * y1)) == (- 1_No) + (- ((x1 * y1) + ((- x) * y1))) by SURREALR:43;
then A3: - (x1 * ((1_No + ((x1 + (- x)) * y1)) * Ix1)) == (- 1_No) + (- ((x1 * y1) + ((- x) * y1))) by A2, SURREALO:4;
A4: x1 * (- ((1_No + ((x1 + (- x)) * y1)) * Ix1)) == (- 1_No) + (- ((x1 * y1) + ((- x) * y1))) by A3, SURREALR:58;
( x1 * (y + (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) == (x1 * y) + (x1 * (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) & (x1 * y) + (x1 * (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) == (x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1)))) ) by A4, SURREALR:43, SURREALR:67;
then x1 * (y + (- ((1_No + ((x1 + (- x)) * y1)) * Ix1))) == (x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1)))) by SURREALO:4;
then A5: 1_No + (x1 * (y + (- ((1_No + ((x1 + (- x)) * y1)) * Ix1)))) == 1_No + ((x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1))))) by SURREALR:43;
A6: 1_No - 1_No == 0_No by SURREALR:39;
- ((- x) * y1) = - (- (x * y1)) by SURREALR:58
.= x * y1 ;
then A7: (x1 * y) + (- ((x1 * y1) + ((- x) * y1))) = (x1 * y) + ((- (x1 * y1)) + (x * y1)) by SURREALR:40
.= ((x1 * y) + (x * y1)) + (- (x1 * y1)) by SURREALR:37 ;
1_No + ((x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1))))) = 1_No + ((- 1_No) + ((x1 * y) + (- ((x1 * y1) + ((- x) * y1))))) by SURREALR:37
.= (1_No + (- 1_No)) + ((x1 * y) + (- ((x1 * y1) + ((- x) * y1)))) by SURREALR:37 ;
then ( 1_No + ((x1 * y) + ((- 1_No) + (- ((x1 * y1) + ((- x) * y1))))) == 0_No + (((x1 * y) + (x * y1)) + (- (x1 * y1))) & 0_No + (((x1 * y) + (x * y1)) + (- (x1 * y1))) = ((x1 * y) + (x * y1)) + (- (x1 * y1)) ) by A7, A6, SURREALR:43;
hence ((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1))) by A5, SURREALO:4; :: thesis: verum