let M1, M2 be ManySortedSet of DYADIC ; :: thesis: ( ( for i, j being Integer
for p being Nat holds
( M1 . i = uInt . i & M1 . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(M1 . (j / (2 |^ p)))},{(M1 . ((j + 1) / (2 |^ p)))}] ) ) & ( for i, j being Integer
for p being Nat holds
( M2 . i = uInt . i & M2 . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(M2 . (j / (2 |^ p)))},{(M2 . ((j + 1) / (2 |^ p)))}] ) ) implies M1 = M2 )
assume that
A59: for i, j being Integer
for p being Nat holds
( M1 . i = uInt . i & M1 . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(M1 . (j / (2 |^ p)))},{(M1 . ((j + 1) / (2 |^ p)))}] ) and
A60: for i, j being Integer
for p being Nat holds
( M2 . i = uInt . i & M2 . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(M2 . (j / (2 |^ p)))},{(M2 . ((j + 1) / (2 |^ p)))}] ) ; :: thesis: M1 = M2
defpred S₁[ Nat] means for d being Dyadic st d in DYADIC $1 holds
M1 . d = M2 . d;
A61: S₁[ 0 ]

proof

let d be Dyadic; :: thesis: ( d in DYADIC 0 implies M1 . d = M2 . d )
assume d in DYADIC 0 ; :: thesis: M1 . d = M2 . d
then ( M1 . d = uInt . d & uInt . d = M2 . d ) by Th21, A59, A60;
hence M1 . d = M2 . d ; :: thesis: verum

end;

A62: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A63: S₁[n] ; :: thesis: S₁[n + 1]
let d be Dyadic; :: thesis: ( d in DYADIC (n + 1) implies M1 . d = M2 . d )
assume A64: d in DYADIC (n + 1) ; :: thesis: M1 . d = M2 . d

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

suppose d in DYADIC n ; :: thesis: M1 . d = M2 . d

hence M1 . d = M2 . d by A63; :: thesis: verum

end;

suppose not d in DYADIC n ; :: thesis: M1 . d = M2 . d

then d in (DYADIC (n + 1)) \ (DYADIC n) by A64, XBOOLE_0:def 5;
then consider i being Integer such that
A65: d = ((2 * i) + 1) / (2 |^ (n + 1)) by Th20;
( i / (2 |^ n) in DYADIC n & (i + 1) / (2 |^ n) in DYADIC n ) by Def4;
then ( M1 . (i / (2 |^ n)) = M2 . (i / (2 |^ n)) & M1 . ((i + 1) / (2 |^ n)) = M2 . ((i + 1) / (2 |^ n)) ) by A63;
then M1 . d = [{(M2 . (i / (2 |^ n)))},{(M2 . ((i + 1) / (2 |^ n)))}] by A65, A59;
hence M1 . d = M2 . d by A65, A60; :: thesis: verum

end;

end;

end;

A66: for n being Nat holds S₁[n] from NAT_1:sch 2(A61, A62);
A67: ( dom M1 = DYADIC & DYADIC = dom M2 ) by PARTFUN1:def 2;
for o being object st o in DYADIC holds
M1 . o = M2 . o

proof

let o be object ; :: thesis: ( o in DYADIC implies M1 . o = M2 . o )
assume o in DYADIC ; :: thesis: M1 . o = M2 . o
then consider i being Integer, n being Nat such that
A68: o = i / (2 |^ n) by Th18;
o in DYADIC n by A68, Def4;
hence M1 . o = M2 . o by A66; :: thesis: verum

end;

hence M1 = M2 by A67, FUNCT_1:2; :: thesis: verum