let d be Dyadic; :: thesis: uDyadic . (- d) = - (uDyadic . d)
defpred S₁[ Nat] means for d being Dyadic st d in DYADIC $1 holds
uDyadic . (- d) = - (uDyadic . d);
A1: S₁[ 0 ]

proof

let d be Dyadic; :: thesis: ( d in DYADIC 0 implies uDyadic . (- d) = - (uDyadic . d) )
assume d in DYADIC 0 ; :: thesis: uDyadic . (- d) = - (uDyadic . d)
then reconsider i = d as Integer by Th21;
( uDyadic . (- d) = uInt . (- i) & uInt . (- i) = - (uInt . i) ) by Def5, Th12;
hence uDyadic . (- d) = - (uDyadic . d) by Def5; :: thesis: verum

end;

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 d be Dyadic; :: thesis: ( d in DYADIC (n + 1) implies uDyadic . (- d) = - (uDyadic . d) )
assume A4: d in DYADIC (n + 1) ; :: thesis: uDyadic . (- d) = - (uDyadic . d)

per cases ( d in DYADIC n or not d in DYADIC n ) ;

suppose d in DYADIC n ; :: thesis: uDyadic . (- d) = - (uDyadic . d)

hence uDyadic . (- d) = - (uDyadic . d) by A3; :: thesis: verum

end;

suppose not d in DYADIC n ; :: thesis: uDyadic . (- d) = - (uDyadic . d)

then d in (DYADIC (n + 1)) \ (DYADIC n) by A4, XBOOLE_0:def 5;
then consider i being Integer such that
A5: d = ((2 * i) + 1) / (2 |^ (n + 1)) by Th20;
set j = - (i + 1);
(2 * (- (i + 1))) + 1 = - ((2 * i) + 1) ;
then A6: - d = ((2 * (- (i + 1))) + 1) / (2 |^ (n + 1)) by A5, XCMPLX_1:187;
A7: - (i / (2 |^ n)) = (- i) / (2 |^ n) by XCMPLX_1:187
.= ((- (i + 1)) + 1) / (2 |^ n) ;
A8: - ((i + 1) / (2 |^ n)) = (- (i + 1)) / (2 |^ n) by XCMPLX_1:187;
( i / (2 |^ n) in DYADIC n & (i + 1) / (2 |^ n) in DYADIC n ) by Def4;
then A9: ( - (uDyadic . (i / (2 |^ n))) = uDyadic . (((- (i + 1)) + 1) / (2 |^ n)) & - (uDyadic . ((i + 1) / (2 |^ n))) = uDyadic . ((- (i + 1)) / (2 |^ n)) ) by A3, A7, A8;
uDyadic . d = [{(uDyadic . (i / (2 |^ n)))},{(uDyadic . ((i + 1) / (2 |^ n)))}] by A5, Def5;
then ( L_ (uDyadic . d) = {(uDyadic . (i / (2 |^ n)))} & R_ (uDyadic . d) = {(uDyadic . ((i + 1) / (2 |^ n)))} ) ;
hence - (uDyadic . d) = [(-- {(uDyadic . ((i + 1) / (2 |^ n)))}),(-- {(uDyadic . (i / (2 |^ n)))})] by SURREALR:7
.= [{(- (uDyadic . ((i + 1) / (2 |^ n))))},(-- {(uDyadic . (i / (2 |^ n)))})] by SURREALR:21
.= [{(- (uDyadic . ((i + 1) / (2 |^ n))))},{(- (uDyadic . (i / (2 |^ n))))}] by SURREALR:21
.= uDyadic . (- d) by A9, A6, Def5 ;
:: thesis: verum

end;

end;

end;

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