let i be Integer; :: thesis: for r being Real holds sReal . (r * i) == (sReal . r) * (uDyadic . i)
let r be Real; :: thesis: sReal . (r * i) == (sReal . r) * (uDyadic . i)
defpred S₁[ Nat] means sReal . ($1 * r) == (sReal . r) * (uDyadic . $1);
A1: uDyadic . 1 = 1_No by Th11, Def5;
A2: ( uDyadic . 0 = uInt . 0 & uInt . 0 = 0_No ) by Def5, Def1;
A3: S₁[ 0 ] by A2, Th46;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
(n + 1) * r = (n * r) + r ;
then A6: sReal . ((n + 1) * r) == (sReal . (n * r)) + (sReal . r) by Lm13;
( (sReal . (n * r)) + (sReal . r) == ((sReal . r) * (uDyadic . n)) + ((sReal . r) * 1_No) & ((sReal . r) * (uDyadic . n)) + ((sReal . r) * 1_No) == (sReal . r) * ((uDyadic . n) + 1_No) ) by A5, SURREALR:66, SURREALR:67;
then (sReal . (n * r)) + (sReal . r) == (sReal . r) * ((uDyadic . n) + 1_No) by SURREALO:4;
then A7: sReal . ((n + 1) * r) == (sReal . r) * ((uDyadic . n) + 1_No) by A6, SURREALO:4;
(sReal . r) * ((uDyadic . n) + 1_No) == (sReal . r) * (uDyadic . (n + 1)) by SURREALR:51, A1, Th39;
then sReal . ((n + 1) * r) == (sReal . r) * (uDyadic . (n + 1)) by A7, SURREALO:4;
hence S₁[n + 1] ; :: thesis: verum

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
consider n being Nat such that
A9: ( n = i or i = - n ) by INT_1:2;

per cases ( n = i or i = - n ) by A9;

suppose n = i ; :: thesis: sReal . (r * i) == (sReal . r) * (uDyadic . i)

hence sReal . (r * i) == (sReal . r) * (uDyadic . i) by A8; :: thesis: verum

end;

suppose A10: i = - n ; :: thesis: sReal . (r * i) == (sReal . r) * (uDyadic . i)

then A11: - (uDyadic . n) = uDyadic . i by Th27;
A12: ( - (sReal . (n * r)) == - ((sReal . r) * (uDyadic . n)) & - ((sReal . r) * (uDyadic . n)) = (sReal . r) * (- (uDyadic . n)) ) by A8, SURREALR:58, SURREALR:65;
- (sReal . (n * r)) == sReal . (- (n * r)) by Lm14;
hence sReal . (r * i) == (sReal . r) * (uDyadic . i) by A10, A11, A12, SURREALO:4; :: thesis: verum

end;

end;