let r be Real; sReal . (r / 2) == (sReal . r) * (uDyadic . (1 / (2 |^ 1)))
set r2 = r / 2;
(r / 2) + (r / 2) = r
;
then A1:
(sReal . (r / 2)) + (sReal . (r / 2)) == sReal . r
by Lm13;
1_No * (sReal . (r / 2)) = sReal . (r / 2)
;
then A2:
(sReal . (r / 2)) + (sReal . (r / 2)) == (sReal . (r / 2)) * (1_No + 1_No)
by SURREALR:67;
( 1_No + 1_No = uInt . (1 + 1) & uInt . (1 + 1) = uDyadic . 2 )
by Th11, Def5, Th13;
then
sReal . r == (sReal . (r / 2)) * (uDyadic . 2)
by A1, A2, SURREALO:4;
then
( (sReal . r) * (uDyadic . (1 / (2 |^ 1))) == ((sReal . (r / 2)) * (uDyadic . 2)) * (uDyadic . (1 / (2 |^ 1))) & ((sReal . (r / 2)) * (uDyadic . 2)) * (uDyadic . (1 / (2 |^ 1))) == (sReal . (r / 2)) * ((uDyadic . 2) * (uDyadic . (1 / (2 |^ 1)))) )
by SURREALR:51, SURREALR:69;
then A3:
(sReal . r) * (uDyadic . (1 / (2 |^ 1))) == (sReal . (r / 2)) * ((uDyadic . 2) * (uDyadic . (1 / (2 |^ 1))))
by SURREALO:4;
2 * (1 / (2 |^ 1)) = 1
;
then
( (uDyadic . 2) * (uDyadic . (1 / (2 |^ 1))) == uDyadic . 1 & uDyadic . 1 = uInt . 1 )
by Th40, Def5;
then
( (sReal . (r / 2)) * ((uDyadic . 2) * (uDyadic . (1 / (2 |^ 1)))) == (sReal . (r / 2)) * 1_No & (sReal . (r / 2)) * 1_No = sReal . (r / 2) )
by Th11, SURREALR:51;
hence
sReal . (r / 2) == (sReal . r) * (uDyadic . (1 / (2 |^ 1)))
by A3, SURREALO:4; verum