defpred S₁[ object , object ] means for n being Nat st $1 = n holds
( $2 is Function of (Funcs ((DYADIC n),(Games (NAT (+) n)))),(Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1))))) & ( for T being Function of (Funcs ((DYADIC n),(Games (NAT (+) n)))),(Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1))))) st T = $2 holds
for f being Function of (DYADIC n),(Games (NAT (+) n)) holds
( ( for d being Dyadic st d in DYADIC n holds
(T . f) . d = f . d ) & ( for i being Integer holds (T . f) . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) ) ) );
A1: for e being object st e in NAT holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in NAT implies ex u being object st S₁[e,u] )
assume A2: e in NAT ; :: thesis: ex u being object st S₁[e,u]
reconsider n = e as Nat by A2;
set n1 = n + 1;
defpred S₂[ object , object ] means ( $2 is Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) & ( for f being Function of (DYADIC n),(Games (NAT (+) n)) st f = $1 holds
for g being Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) st g = $2 holds
( ( for d being Dyadic st d in DYADIC n holds
g . d = f . d ) & ( for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) ) ) );
A3: for c being object st c in Funcs ((DYADIC n),(Games (NAT (+) n))) holds
ex u being object st S₂[c,u]

proof

let c be object ; :: thesis: ( c in Funcs ((DYADIC n),(Games (NAT (+) n))) implies ex u being object st S₂[c,u] )
assume A4: c in Funcs ((DYADIC n),(Games (NAT (+) n))) ; :: thesis: ex u being object st S₂[c,u]
reconsider C = c as Function of (DYADIC n),(Games (NAT (+) n)) by A4, FUNCT_2:66;
defpred S₃[ object , object ] means ( ( $1 in DYADIC n implies $2 = C . $1 ) & ( not $1 in DYADIC n implies for i being Integer st $1 = ((2 * i) + 1) / (2 |^ (n + 1)) holds
$2 = [{(C . (i / (2 |^ n)))},{(C . ((i + 1) / (2 |^ n)))}] ) );
A5: for e being object st e in DYADIC (n + 1) holds
ex u being object st S₃[e,u]

proof

let e be object ; :: thesis: ( e in DYADIC (n + 1) implies ex u being object st S₃[e,u] )
assume A6: e in DYADIC (n + 1) ; :: thesis: ex u being object st S₃[e,u]
reconsider d = e as Dyadic by A6;

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

suppose A7: e in DYADIC n ; :: thesis: ex u being object st S₃[e,u]

take C . e ; :: thesis: S₃[e,C . e]
thus S₃[e,C . e] by A7; :: thesis: verum

end;

suppose A8: not e in DYADIC n ; :: thesis: ex u being object st S₃[e,u]

then d in (DYADIC (n + 1)) \ (DYADIC n) by A6, XBOOLE_0:def 5;
then consider i being Integer such that
A9: d = ((2 * i) + 1) / (2 |^ (n + 1)) by Th20;
take X = [{(C . (i / (2 |^ n)))},{(C . ((i + 1) / (2 |^ n)))}]; :: thesis: S₃[e,X]
thus ( e in DYADIC n implies X = C . e ) by A8; :: thesis: ( not e in DYADIC n implies for i being Integer st e = ((2 * i) + 1) / (2 |^ (n + 1)) holds
X = [{(C . (i / (2 |^ n)))},{(C . ((i + 1) / (2 |^ n)))}] )
assume not e in DYADIC n ; :: thesis: for i being Integer st e = ((2 * i) + 1) / (2 |^ (n + 1)) holds
X = [{(C . (i / (2 |^ n)))},{(C . ((i + 1) / (2 |^ n)))}]
let j be Integer; :: thesis: ( e = ((2 * j) + 1) / (2 |^ (n + 1)) implies X = [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}] )
assume A10: e = ((2 * j) + 1) / (2 |^ (n + 1)) ; :: thesis: X = [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]
((2 * i) + 1) * (2 |^ (n + 1)) = ((2 * j) + 1) * (2 |^ (n + 1)) by A10, A9, XCMPLX_1:95;
then (2 * i) + 1 = (2 * j) + 1 by XCMPLX_1:5;
hence X = [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}] ; :: thesis: verum

end;

end;

end;

consider d being Function such that
A11: dom d = DYADIC (n + 1) and
A12: for e being object st e in DYADIC (n + 1) holds
S₃[e,d . e] from CLASSES1:sch 1(A5);
take d ; :: thesis: S₂[c,d]
A13: dom C = DYADIC n by FUNCT_2:def 1;
rng d c= Games (NAT (+) (n + 1))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng d or y in Games (NAT (+) (n + 1)) )
assume y in rng d ; :: thesis: y in Games (NAT (+) (n + 1))
then consider x being object such that
A14: ( x in dom d & d . x = y ) by FUNCT_1:def 3;
reconsider x = x as Dyadic by A14, A11;

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

suppose A15: x in DYADIC n ; :: thesis: y in Games (NAT (+) (n + 1))

then C . x in rng C by A13, FUNCT_1:def 3;
then A16: C . x in Games (NAT (+) n) ;
A17: d . x = C . x by A11, A12, A14, A15;
n < n + 1 by NAT_1:13;
then Segm n c= Segm (n + 1) by NAT_1:39;
then Games (NAT (+) n) c= Games (NAT (+) (n + 1)) by SURREAL0:1, ORDINAL7:95;
hence y in Games (NAT (+) (n + 1)) by A17, A14, A16; :: thesis: verum

end;

suppose A18: not x in DYADIC n ; :: thesis: y in Games (NAT (+) (n + 1))

then x in (DYADIC (n + 1)) \ (DYADIC n) by A14, A11, XBOOLE_0:def 5;
then consider j being Integer such that
A19: x = ((2 * j) + 1) / (2 |^ (n + 1)) by Th20;
set O = [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}];
A20: d . x = [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}] by A19, A18, A14, A11, A12;
( j / (2 |^ n) in DYADIC n & (j + 1) / (2 |^ n) in DYADIC n ) by Def4;
then ( C . (j / (2 |^ n)) in rng C & C . ((j + 1) / (2 |^ n)) in rng C ) by A13, FUNCT_1:def 3;
then A21: ( C . (j / (2 |^ n)) in Games (NAT (+) n) & C . ((j + 1) / (2 |^ n)) in Games (NAT (+) n) ) ;
for a being object st a in (L_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]) \/ (R_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]) holds
ex A being Ordinal st
( A in NAT (+) (n + 1) & a in Games A )

proof

let a be object ; :: thesis: ( a in (L_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]) \/ (R_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]) implies ex A being Ordinal st
( A in NAT (+) (n + 1) & a in Games A ) )
assume a in (L_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]) \/ (R_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}]) ; :: thesis: ex A being Ordinal st
( A in NAT (+) (n + 1) & a in Games A )
then A22: ( a in L_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}] or a in R_ [{(C . (j / (2 |^ n)))},{(C . ((j + 1) / (2 |^ n)))}] ) by XBOOLE_0:def 3;
take A = NAT (+) n; :: thesis: ( A in NAT (+) (n + 1) & a in Games A )
n < n + 1 by NAT_1:13;
then n in Segm (n + 1) by NAT_1:44;
hence ( A in NAT (+) (n + 1) & a in Games A ) by A22, A21, TARSKI:def 1, ORDINAL7:94; :: thesis: verum

end;

hence y in Games (NAT (+) (n + 1)) by A20, A14, SURREAL0:4; :: thesis: verum

end;

end;

end;

hence d is Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) by A11, FUNCT_2:2; :: thesis: for f being Function of (DYADIC n),(Games (NAT (+) n)) st f = c holds
for g being Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) st g = d holds
( ( for d being Dyadic st d in DYADIC n holds
g . d = f . d ) & ( for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) )
let f be Function of (DYADIC n),(Games (NAT (+) n)); :: thesis: ( f = c implies for g being Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) st g = d holds
( ( for d being Dyadic st d in DYADIC n holds
g . d = f . d ) & ( for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) ) )
assume A23: f = c ; :: thesis: for g being Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) st g = d holds
( ( for d being Dyadic st d in DYADIC n holds
g . d = f . d ) & ( for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) )
let g be Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))); :: thesis: ( g = d implies ( ( for d being Dyadic st d in DYADIC n holds
g . d = f . d ) & ( for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) ) )
assume A24: g = d ; :: thesis: ( ( for d being Dyadic st d in DYADIC n holds
g . d = f . d ) & ( for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] ) )
DYADIC n c= DYADIC (n + 1) by Th19, NAT_1:11;
hence for z being Dyadic st z in DYADIC n holds
g . z = f . z by A12, A23, A24; :: thesis: for i being Integer holds g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}]
let i be Integer; :: thesis: g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}]
set I = ((2 * i) + 1) / (2 |^ (n + 1));
((2 * i) + 1) / (2 |^ (n + 1)) in (DYADIC (n + 1)) \ (DYADIC n) by Th20;
then ( ((2 * i) + 1) / (2 |^ (n + 1)) in DYADIC (n + 1) & not ((2 * i) + 1) / (2 |^ (n + 1)) in DYADIC n ) by XBOOLE_0:def 5;
hence g . (((2 * i) + 1) / (2 |^ (n + 1))) = [{(f . (i / (2 |^ n)))},{(f . ((i + 1) / (2 |^ n)))}] by A12, A23, A24; :: thesis: verum

end;

consider H being Function such that
A25: dom H = Funcs ((DYADIC n),(Games (NAT (+) n))) and
A26: for e being object st e in Funcs ((DYADIC n),(Games (NAT (+) n))) holds
S₂[e,H . e] from CLASSES1:sch 1(A3);
take H ; :: thesis: S₁[e,H]
let k be Nat; :: thesis: ( e = k implies ( H is Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) & ( for T being Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) st T = H holds
for f being Function of (DYADIC k),(Games (NAT (+) k)) holds
( ( for d being Dyadic st d in DYADIC k holds
(T . f) . d = f . d ) & ( for i being Integer holds (T . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) ) ) ) )
assume A27: e = k ; :: thesis: ( H is Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) & ( for T being Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) st T = H holds
for f being Function of (DYADIC k),(Games (NAT (+) k)) holds
( ( for d being Dyadic st d in DYADIC k holds
(T . f) . d = f . d ) & ( for i being Integer holds (T . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) ) ) )
rng H c= Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1))))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng H or y in Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1)))) )
assume y in rng H ; :: thesis: y in Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1))))
then consider x being object such that
A28: ( x in dom H & H . x = y ) by FUNCT_1:def 3;
reconsider hx = H . x as Function of (DYADIC (n + 1)),(Games (NAT (+) (n + 1))) by A28, A25, A26;
hx in Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1)))) by FUNCT_2:8;
hence y in Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1)))) by A28; :: thesis: verum

end;

then reconsider h = H as Function of (Funcs ((DYADIC n),(Games (NAT (+) n)))),(Funcs ((DYADIC (n + 1)),(Games (NAT (+) (n + 1))))) by A25, FUNCT_2:2;
h = H ;
hence H is Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) by A27; :: thesis: for T being Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) st T = H holds
for f being Function of (DYADIC k),(Games (NAT (+) k)) holds
( ( for d being Dyadic st d in DYADIC k holds
(T . f) . d = f . d ) & ( for i being Integer holds (T . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) )
let G be Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))); :: thesis: ( G = H implies for f being Function of (DYADIC k),(Games (NAT (+) k)) holds
( ( for d being Dyadic st d in DYADIC k holds
(G . f) . d = f . d ) & ( for i being Integer holds (G . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) ) )
assume A29: G = H ; :: thesis: for f being Function of (DYADIC k),(Games (NAT (+) k)) holds
( ( for d being Dyadic st d in DYADIC k holds
(G . f) . d = f . d ) & ( for i being Integer holds (G . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) )
let f be Function of (DYADIC k),(Games (NAT (+) k)); :: thesis: ( ( for d being Dyadic st d in DYADIC k holds
(G . f) . d = f . d ) & ( for i being Integer holds (G . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) )
f in dom H by A27, A25, FUNCT_2:8;
then S₂[f,H . f] by A25, A26;
hence ( ( for d being Dyadic st d in DYADIC k holds
(G . f) . d = f . d ) & ( for i being Integer holds (G . f) . (((2 * i) + 1) / (2 |^ (k + 1))) = [{(f . (i / (2 |^ k)))},{(f . ((i + 1) / (2 |^ k)))}] ) ) by A27, A29; :: thesis: verum

end;

consider P being Function such that
A30: dom P = NAT and
A31: for e being object st e in NAT holds
S₁[e,P . e] from CLASSES1:sch 1(A1);
P is Function-yielding

proof

let o be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not o in dom P or P . o is set )
thus ( not o in dom P or P . o is set ) by A30, A31; :: thesis: verum

end;

then reconsider P = P as Function-yielding Function ;
A32: dom uInt = INT by PARTFUN1:def 2;
A33: ( rng uInt c= Games NAT & NAT = NAT (+) 0 ) by Th22, XBOOLE_1:1, ORDINAL7:69;
deffunc H₁( object , object ) -> set = (P . $1) . $2;
consider f1 being Function such that
A34: ( dom f1 = NAT & f1 . 0 = uInt ) and
A35: for n being Nat holds f1 . (n + 1) = H₁(n,f1 . n) from NAT_1:sch 11();
defpred S₂[ Nat] means f1 . $1 is Function of (DYADIC $1),(Games (NAT (+) $1));
A36: S₂[ 0 ] by A33, A32, FUNCT_2:2, Th21, A34;
A37: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A38: S₂[k] ; :: thesis: S₂[k + 1]
reconsider f1k = f1 . k as Function of (DYADIC k),(Games (NAT (+) k)) by A38;
set k1 = k + 1;
k in NAT by ORDINAL1:def 12;
then reconsider Pk = P . k as Function of (Funcs ((DYADIC k),(Games (NAT (+) k)))),(Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1))))) by A31;
dom Pk = Funcs ((DYADIC k),(Games (NAT (+) k))) by FUNCT_2:def 1;
then A39: f1k in dom Pk by FUNCT_2:8;
f1 . (k + 1) = Pk . f1k by A35;
then ( f1 . (k + 1) in rng Pk & rng Pk c= Funcs ((DYADIC (k + 1)),(Games (NAT (+) (k + 1)))) ) by A39, FUNCT_1:def 3;
hence S₂[k + 1] by FUNCT_2:66; :: thesis: verum

end;

A40: for k being Nat holds S₂[k] from NAT_1:sch 2(A36, A37);
f1 is Function-yielding

proof

let o be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not o in dom f1 or f1 . o is set )
assume o in dom f1 ; :: thesis: f1 . o is set
then reconsider n = o as Nat by A34;
S₂[n] by A40;
hence f1 . o is set ; :: thesis: verum

end;

then reconsider f1 = f1 as Function-yielding Function ;
defpred S₃[ object , object ] means for n being Nat st $1 in DYADIC n holds
$2 = (f1 . n) . $1;
A41: for d being Dyadic
for n being Nat st d in DYADIC n holds
for m being Nat holds (f1 . n) . d = (f1 . (n + m)) . d

proof

let d be Dyadic; :: thesis: for n being Nat st d in DYADIC n holds
for m being Nat holds (f1 . n) . d = (f1 . (n + m)) . d
let n be Nat; :: thesis: ( d in DYADIC n implies for m being Nat holds (f1 . n) . d = (f1 . (n + m)) . d )
assume A42: d in DYADIC n ; :: thesis: for m being Nat holds (f1 . n) . d = (f1 . (n + m)) . d
defpred S₄[ Nat] means (f1 . n) . d = (f1 . (n + $1)) . d;
A43: S₄[ 0 ] ;
A44: for m being Nat st S₄[m] holds
S₄[m + 1]

proof

let m be Nat; :: thesis: ( S₄[m] implies S₄[m + 1] )
assume A45: S₄[m] ; :: thesis: S₄[m + 1]
set nm = n + m;
A46: n + m in NAT by ORDINAL1:def 12;
then reconsider Pnm = P . (n + m) as Function of (Funcs ((DYADIC (n + m)),(Games (NAT (+) (n + m))))),(Funcs ((DYADIC ((n + m) + 1)),(Games (NAT (+) ((n + m) + 1))))) by A31;
reconsider f1nm = f1 . (n + m) as Function of (DYADIC (n + m)),(Games (NAT (+) (n + m))) by A40;
DYADIC n c= DYADIC (n + m) by NAT_1:11, Th19;
then (Pnm . f1nm) . d = f1nm . d by A46, A31, A42;
hence S₄[m + 1] by A45, A35; :: thesis: verum

end;

for m being Nat holds S₄[m] from NAT_1:sch 2(A43, A44);
hence for m being Nat holds (f1 . n) . d = (f1 . (n + m)) . d ; :: thesis: verum

end;

A47: for e being object st e in DYADIC holds
ex u being object st S₃[e,u]

proof

let e be object ; :: thesis: ( e in DYADIC implies ex u being object st S₃[e,u] )
assume A48: e in DYADIC ; :: thesis: ex u being object st S₃[e,u]
reconsider d = e as Dyadic by A48;

per cases ( d is Integer or ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1)) ) by Th23;

suppose A49: d is Integer ; :: thesis: ex u being object st S₃[e,u]

take sd = uInt . d; :: thesis: S₃[e,sd]
let m be Nat; :: thesis: ( e in DYADIC m implies sd = (f1 . m) . e )
assume e in DYADIC m ; :: thesis: sd = (f1 . m) . e
(f1 . 0) . d = (f1 . (0 + m)) . d by A49, A41, INT_1:def 2, Th21;
hence sd = (f1 . m) . e by A34; :: thesis: verum

end;

suppose ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1)) ; :: thesis: ex u being object st S₃[e,u]

then consider p being Nat, i being Integer such that
A50: d = ((2 * i) + 1) / (2 |^ (p + 1)) ;
A51: d in (DYADIC (p + 1)) \ (DYADIC p) by A50, Th20;
then A52: ( d in DYADIC (p + 1) & not d in DYADIC p ) by XBOOLE_0:def 5;
take sd = (f1 . (p + 1)) . d; :: thesis: S₃[e,sd]
let m be Nat; :: thesis: ( e in DYADIC m implies sd = (f1 . m) . e )
assume A53: e in DYADIC m ; :: thesis: sd = (f1 . m) . e
p + 1 <= m

proof

assume m < p + 1 ; :: thesis: contradiction
then m <= p by NAT_1:13;
then DYADIC m c= DYADIC p by Th19;
hence contradiction by A53, A51, XBOOLE_0:def 5; :: thesis: verum

end;

then reconsider r = m - (p + 1) as Nat by NAT_1:21;
(p + 1) + r = m ;
hence sd = (f1 . m) . e by A41, A52; :: thesis: verum

end;

end;

end;

consider K being Function such that
A54: dom K = DYADIC and
A55: for e being object st e in DYADIC holds
S₃[e,K . e] from CLASSES1:sch 1(A47);
reconsider K = K as ManySortedSet of DYADIC by PARTFUN1:def 2, A54, RELAT_1:def 18;
take K ; :: thesis: for i, j being Integer
for p being Nat holds
( K . i = uInt . i & K . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(K . (j / (2 |^ p)))},{(K . ((j + 1) / (2 |^ p)))}] )
let i, j be Integer; :: thesis: for p being Nat holds
( K . i = uInt . i & K . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(K . (j / (2 |^ p)))},{(K . ((j + 1) / (2 |^ p)))}] )
let p be Nat; :: thesis: ( K . i = uInt . i & K . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(K . (j / (2 |^ p)))},{(K . ((j + 1) / (2 |^ p)))}] )
set p1 = p + 1;
( i in INT & INT = DYADIC 0 ) by INT_1:def 2, Th21;
hence K . i = uInt . i by A34, A55; :: thesis: K . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(K . (j / (2 |^ p)))},{(K . ((j + 1) / (2 |^ p)))}]
set D = ((2 * j) + 1) / (2 |^ (p + 1));
((2 * j) + 1) / (2 |^ (p + 1)) in (DYADIC (p + 1)) \ (DYADIC p) by Th20;
then ( ((2 * j) + 1) / (2 |^ (p + 1)) in DYADIC (p + 1) & not ((2 * j) + 1) / (2 |^ (p + 1)) in DYADIC p ) by XBOOLE_0:def 5;
then A56: K . (((2 * j) + 1) / (2 |^ (p + 1))) = (f1 . (p + 1)) . (((2 * j) + 1) / (2 |^ (p + 1))) by A55;
A57: p in NAT by ORDINAL1:def 12;
then reconsider Pp = P . p as Function of (Funcs ((DYADIC p),(Games (NAT (+) p)))),(Funcs ((DYADIC (p + 1)),(Games (NAT (+) (p + 1))))) by A31;
reconsider f1p = f1 . p as Function of (DYADIC p),(Games (NAT (+) p)) by A40;
A58: (Pp . f1p) . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(f1p . (j / (2 |^ p)))},{(f1p . ((j + 1) / (2 |^ p)))}] by A57, A31;
( j / (2 |^ p) in DYADIC p & (j + 1) / (2 |^ p) in DYADIC p ) by Def4;
then ( K . (j / (2 |^ p)) = f1p . (j / (2 |^ p)) & K . ((j + 1) / (2 |^ p)) = f1p . ((j + 1) / (2 |^ p)) ) by A55;
hence K . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(K . (j / (2 |^ p)))},{(K . ((j + 1) / (2 |^ p)))}] by A56, A58, A35; :: thesis: verum