let x, y be Surreal; :: thesis: for a, b, c, d, e being Real holds ((uReal . (a - b)) * (x + ((uReal . (c + d)) * y))) + ((uReal . b) * (x + ((uReal . (c - e)) * y))) == ((uReal . a) * x) + ((uReal . (((a * c) - (b * e)) + (d * (a - b)))) * y)
let a, b, c, d, e be Real; :: thesis: ((uReal . (a - b)) * (x + ((uReal . (c + d)) * y))) + ((uReal . b) * (x + ((uReal . (c - e)) * y))) == ((uReal . a) * x) + ((uReal . (((a * c) - (b * e)) + (d * (a - b)))) * y)
A1: (uReal . (a - b)) * (x + ((uReal . (c + d)) * y)) == ((uReal . (a - b)) * x) + ((uReal . (a - b)) * ((uReal . (c + d)) * y)) by SURREALR:67;
( (uReal . (a - b)) * ((uReal . (c + d)) * y) == ((uReal . (a - b)) * (uReal . (c + d))) * y & ((uReal . (a - b)) * (uReal . (c + d))) * y == (uReal . ((a - b) * (c + d))) * y ) by SURREALN:57, SURREALR:54, SURREALR:69;
then (uReal . (a - b)) * ((uReal . (c + d)) * y) == (uReal . ((a - b) * (c + d))) * y by SURREALO:9;
then ((uReal . (a - b)) * x) + ((uReal . (a - b)) * ((uReal . (c + d)) * y)) == ((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y) by SURREALR:43;
then A2: (uReal . (a - b)) * (x + ((uReal . (c + d)) * y)) == ((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y) by A1, SURREALO:9;
A3: (uReal . b) * (x + ((uReal . (c - e)) * y)) == ((uReal . b) * x) + ((uReal . b) * ((uReal . (c - e)) * y)) by SURREALR:67;
( (uReal . b) * ((uReal . (c - e)) * y) == ((uReal . b) * (uReal . (c - e))) * y & ((uReal . b) * (uReal . (c - e))) * y == (uReal . (b * (c - e))) * y ) by SURREALN:57, SURREALR:54, SURREALR:69;
then (uReal . b) * ((uReal . (c - e)) * y) == (uReal . (b * (c - e))) * y by SURREALO:9;
then ((uReal . b) * x) + ((uReal . b) * ((uReal . (c - e)) * y)) == ((uReal . b) * x) + ((uReal . (b * (c - e))) * y) by SURREALR:43;
then (uReal . b) * (x + ((uReal . (c - e)) * y)) == ((uReal . b) * x) + ((uReal . (b * (c - e))) * y) by A3, SURREALO:9;
then A4: ((uReal . (a - b)) * (x + ((uReal . (c + d)) * y))) + ((uReal . b) * (x + ((uReal . (c - e)) * y))) == (((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y)) + (((uReal . b) * x) + ((uReal . (b * (c - e))) * y)) by A2, SURREALR:43;
A5: (((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y)) + ((uReal . b) * x) == ((uReal . ((a - b) + b)) * x) + ((uReal . ((a - b) * (c + d))) * y) by Th30;
(((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y)) + (((uReal . b) * x) + ((uReal . (b * (c - e))) * y)) = ((((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y)) + ((uReal . b) * x)) + ((uReal . (b * (c - e))) * y) by SURREALR:37;
then ( (((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y)) + (((uReal . b) * x) + ((uReal . (b * (c - e))) * y)) == (((uReal . a) * x) + ((uReal . ((a - b) * (c + d))) * y)) + ((uReal . (b * (c - e))) * y) & (((uReal . a) * x) + ((uReal . ((a - b) * (c + d))) * y)) + ((uReal . (b * (c - e))) * y) == ((uReal . a) * x) + ((uReal . (((a - b) * (c + d)) + (b * (c - e)))) * y) ) by Th30, A5, SURREALR:43;
then (((uReal . (a - b)) * x) + ((uReal . ((a - b) * (c + d))) * y)) + (((uReal . b) * x) + ((uReal . (b * (c - e))) * y)) == ((uReal . a) * x) + ((uReal . (((a - b) * (c + d)) + (b * (c - e)))) * y) by SURREALO:4;
hence ((uReal . (a - b)) * (x + ((uReal . (c + d)) * y))) + ((uReal . b) * (x + ((uReal . (c - e)) * y))) == ((uReal . a) * x) + ((uReal . (((a * c) - (b * e)) + (d * (a - b)))) * y) by A4, SURREALO:4; :: thesis: verum