let r1, r2 be Real; :: thesis: for d1, d2 being Dyadic holds (((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2))) + (- ((uDyadic . d1) * (uDyadic . d2))) == sReal . (((d1 * r2) + (r1 * d2)) - (d1 * d2))
let d1, d2 be Dyadic; :: thesis: (((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2))) + (- ((uDyadic . d1) * (uDyadic . d2))) == sReal . (((d1 * r2) + (r1 * d2)) - (d1 * d2))
( (uDyadic . d1) * (sReal . r2) == sReal . (d1 * r2) & (sReal . r1) * (uDyadic . d2) == sReal . (r1 * d2) ) by Lm17;
then ( ((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2)) == (sReal . (d1 * r2)) + (sReal . (r1 * d2)) & (sReal . (d1 * r2)) + (sReal . (r1 * d2)) == sReal . ((d1 * r2) + (r1 * d2)) ) by SURREALR:43, Lm13;
then A1: ((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2)) == sReal . ((d1 * r2) + (r1 * d2)) by SURREALO:4;
( (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) & uDyadic . (d1 * d2) == sReal . (d1 * d2) ) by Th40, Th46;
then (uDyadic . d1) * (uDyadic . d2) == sReal . (d1 * d2) by SURREALO:4;
then ( - ((uDyadic . d1) * (uDyadic . d2)) == - (sReal . (d1 * d2)) & - (sReal . (d1 * d2)) == sReal . (- (d1 * d2)) ) by Lm14, SURREALR:10;
then - ((uDyadic . d1) * (uDyadic . d2)) == sReal . (- (d1 * d2)) by SURREALO:4;
then ( (((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2))) + (- ((uDyadic . d1) * (uDyadic . d2))) == (sReal . ((d1 * r2) + (r1 * d2))) + (sReal . (- (d1 * d2))) & (sReal . ((d1 * r2) + (r1 * d2))) + (sReal . (- (d1 * d2))) == sReal . (((d1 * r2) + (r1 * d2)) + (- (d1 * d2))) ) by A1, SURREALR:43, Lm13;
hence (((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2))) + (- ((uDyadic . d1) * (uDyadic . d2))) == sReal . (((d1 * r2) + (r1 * d2)) - (d1 * d2)) by SURREALO:4; :: thesis: verum