let d be Dyadic; :: thesis: for r being Real holds sReal . (r * d) == (sReal . r) * (uDyadic . d)
let r be Real; :: thesis: sReal . (r * d) == (sReal . r) * (uDyadic . d)
defpred S₁[ Nat] means for r being Real
for d being Dyadic st d in DYADIC $1 holds
sReal . (r * d) == (sReal . r) * (uDyadic . d);
A1: S₁[ 0 ] by Lm15, Th21;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let r be Real; :: thesis: for d being Dyadic st d in DYADIC (n + 1) holds
sReal . (r * d) == (sReal . r) * (uDyadic . d)
let d be Dyadic; :: thesis: ( d in DYADIC (n + 1) implies sReal . (r * d) == (sReal . r) * (uDyadic . d) )
assume A4: d in DYADIC (n + 1) ; :: thesis: sReal . (r * d) == (sReal . r) * (uDyadic . d)
consider i being Integer such that
A5: d = i / (2 |^ (n + 1)) by A4, Def4;
A6: i * 1 = i ;
A7: i / (2 |^ n) in DYADIC n by Def4;
2 |^ (n + 1) = 2 * (2 |^ n) by NEWTON:6;
then A8: d = (i / (2 |^ n)) * (1 / 2) by A6, A5, XCMPLX_1:76;
then r * d = (r / 2) * (i / (2 |^ n)) ;
then A9: sReal . (r * d) == (sReal . (r / 2)) * (uDyadic . (i / (2 |^ n))) by A7, A3;
( (sReal . (r / 2)) * (uDyadic . (i / (2 |^ n))) == ((sReal . r) * (uDyadic . (1 / (2 |^ 1)))) * (uDyadic . (i / (2 |^ n))) & ((sReal . r) * (uDyadic . (1 / (2 |^ 1)))) * (uDyadic . (i / (2 |^ n))) == (sReal . r) * ((uDyadic . (1 / (2 |^ 1))) * (uDyadic . (i / (2 |^ n)))) ) by Lm16, SURREALR:51, SURREALR:69;
then A10: (sReal . (r / 2)) * (uDyadic . (i / (2 |^ n))) == (sReal . r) * ((uDyadic . (1 / (2 |^ 1))) * (uDyadic . (i / (2 |^ n)))) by SURREALO:4;
(sReal . r) * ((uDyadic . (1 / (2 |^ 1))) * (uDyadic . (i / (2 |^ n)))) == (sReal . r) * (uDyadic . d) by A8, Th40, SURREALR:51;
then (sReal . (r / 2)) * (uDyadic . (i / (2 |^ n))) == (sReal . r) * (uDyadic . d) by A10, SURREALO:4;
hence sReal . (r * d) == (sReal . r) * (uDyadic . d) by A9, SURREALO:4; :: thesis: verum

end;

A11: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
consider i being Integer, n being Nat such that
A12: d = i / (2 |^ n) by Th18;
d in DYADIC n by A12, Def4;
hence sReal . (r * d) == (sReal . r) * (uDyadic . d) by A11; :: thesis: verum