defpred S₂[ Function] means for g being ConwayGame st g in dom $1 holds
$1 . g = F₁(g,($1 | (the_proper_Tree_of g)));
defpred S₃[ ConwayGame] means ex f being Function st
( dom f = the_Tree_of $1 & S₂[f] );
defpred S₄[ object , object ] means ex g being ConwayGame st
( $1 = g & ex f being Function st
( $2 = f & dom f = the_Tree_of g & S₂[f] ) );
A1: for g being ConwayGame
for f1, f2 being Function st dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds
f1 . g1 = F₁(g1,(f1 | (the_proper_Tree_of g1))) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = F₁(g1,(f2 | (the_proper_Tree_of g1))) ) holds
f1 = f2 from CGAMES_1:sch 5();
then A2: for x, y, z being object st S₄[x,y] & S₄[x,z] holds
y = z ;
A3: for g being ConwayGame
for f being Function st S₂[f] holds
S₂[f | (the_Tree_of g)]

proof

let g be ConwayGame; :: thesis: for f being Function st S₂[f] holds
S₂[f | (the_Tree_of g)]
let f be Function; :: thesis: ( S₂[f] implies S₂[f | (the_Tree_of g)] )
assume A4: S₂[f] ; :: thesis: S₂[f | (the_Tree_of g)]
let g1 be ConwayGame; :: thesis: ( g1 in dom (f | (the_Tree_of g)) implies (f | (the_Tree_of g)) . g1 = F₁(g1,((f | (the_Tree_of g)) | (the_proper_Tree_of g1))) )
assume A5: g1 in dom (f | (the_Tree_of g)) ; :: thesis: (f | (the_Tree_of g)) . g1 = F₁(g1,((f | (the_Tree_of g)) | (the_proper_Tree_of g1)))
dom (f | (the_Tree_of g)) c= dom f by RELAT_1:60;
then A6: ( f . g1 = F₁(g1,(f | (the_proper_Tree_of g1))) & f . g1 = (f | (the_Tree_of g)) . g1 ) by A4, A5, FUNCT_1:47;
dom (f | (the_Tree_of g)) c= the_Tree_of g by RELAT_1:58;
then the_Tree_of g1 c= the_Tree_of g by Th31, A5;
hence (f | (the_Tree_of g)) . g1 = F₁(g1,((f | (the_Tree_of g)) | (the_proper_Tree_of g1))) by A6, RELAT_1:74, XBOOLE_1:1; :: thesis: verum

end;

A7: for g being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g holds
S₃[gO] ) holds
S₃[g]

proof

let g be ConwayGame; :: thesis: ( ( for gO being ConwayGame st gO in the_Options_of g holds
S₃[gO] ) implies S₃[g] )
assume A8: for gO being ConwayGame st gO in the_Options_of g holds
S₃[gO] ; :: thesis: S₃[g]
consider FUNCS being set such that
A9: for y being object holds
( y in FUNCS iff ex x being object st
( x in the_Tree_of g & S₄[x,y] ) ) from TARSKI:sch 1(A2);
( FUNCS is functional & FUNCS is compatible )

proof

thus FUNCS is functional :: thesis: FUNCS is compatible

proof

let y be object ; :: according to FUNCT_1:def 13 :: thesis: ( not y in FUNCS or y is set )
assume y in FUNCS ; :: thesis: y is set
then ex x being object st
( x in the_Tree_of g & S₄[x,y] ) by A9;
hence y is set ; :: thesis: verum

end;

now :: thesis: for f1, f2 being Function st f1 in FUNCS & f2 in FUNCS holds
f1 tolerates f2

let f1, f2 be Function; :: thesis: ( f1 in FUNCS & f2 in FUNCS implies f1 tolerates f2 )
assume f1 in FUNCS ; :: thesis: ( f2 in FUNCS implies f1 tolerates f2 )
then ex x being object st
( x in the_Tree_of g & S₄[x,f1] ) by A9;
then consider g1 being ConwayGame such that
A10: ( g1 in the_Tree_of g & dom f1 = the_Tree_of g1 & S₂[f1] ) ;
assume f2 in FUNCS ; :: thesis: f1 tolerates f2
then ex x being object st
( x in the_Tree_of g & S₄[x,f2] ) by A9;
then consider g2 being ConwayGame such that
A11: ( g2 in the_Tree_of g & dom f2 = the_Tree_of g2 & S₂[f2] ) ;
thus f1 tolerates f2 :: thesis: verum

proof

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom f1) /\ (dom f2) or f1 . x = f2 . x )
assume x in (dom f1) /\ (dom f2) ; :: thesis: f1 . x = f2 . x
then A12: ( x in the_Tree_of g1 & x in the_Tree_of g2 ) by A10, A11, XBOOLE_0:def 4;
then reconsider g0 = x as ConwayGame ;
set T = the_Tree_of g0;
( the_Tree_of g0 c= dom f1 & the_Tree_of g0 c= dom f2 ) by Th31, A10, A11, A12;
then ( dom (f1 | (the_Tree_of g0)) = the_Tree_of g0 & dom (f2 | (the_Tree_of g0)) = the_Tree_of g0 & S₂[f1 | (the_Tree_of g0)] & S₂[f2 | (the_Tree_of g0)] ) by A3, A10, A11, RELAT_1:62;
then ( f1 | (the_Tree_of g0) = f2 | (the_Tree_of g0) & g0 in dom (f1 | (the_Tree_of g0)) & g0 in dom (f2 | (the_Tree_of g0)) ) by A1, Th24;
then ( f1 | (the_Tree_of g0) = f2 | (the_Tree_of g0) & f1 . g0 = (f1 | (the_Tree_of g0)) . g0 & f2 . g0 = (f2 | (the_Tree_of g0)) . g0 ) by FUNCT_1:47;
hence f1 . x = f2 . x ; :: thesis: verum

end;

end;

hence FUNCS is compatible by COMPUT_1:def 1; :: thesis: verum

end;

then reconsider FS = FUNCS as functional compatible set ;
reconsider f = union FS as Function ;
take f ; :: thesis: ( dom f = the_Tree_of g & S₂[f] )
A13: the_proper_Tree_of g c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_proper_Tree_of g or x in dom f )
assume x in the_proper_Tree_of g ; :: thesis: x in dom f
then ( x in the_Tree_of g & x <> g ) by ZFMISC_1:56;
then consider gO being ConwayGame such that
A14: ( gO in the_Options_of g & x in the_Tree_of gO ) by Th27;
consider fO being Function such that
A15: ( dom fO = the_Tree_of gO & S₂[fO] ) by A8, A14;
the_Options_of g c= the_Tree_of g by Th34;
then fO in FUNCS by A9, A14, A15;
then ( dom fO c= dom f & x in dom fO ) by A14, A15, COMPUT_1:13;
hence x in dom f ; :: thesis: verum

end;

A16: dom f c= the_Tree_of g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in the_Tree_of g )
assume x in dom f ; :: thesis: x in the_Tree_of g
then [x,(f . x)] in f by FUNCT_1:def 2;
then ex y being set st
( [x,(f . x)] in y & y in FUNCS ) by TARSKI:def 4;
then consider f1 being Function such that
A17: ( [x,(f . x)] in f1 & f1 in FUNCS ) ;
ex y being object st
( y in the_Tree_of g & S₄[y,f1] ) by A17, A9;
then consider g1 being ConwayGame such that
A18: ( g1 in the_Tree_of g & dom f1 = the_Tree_of g1 ) ;
( x in dom f1 & dom f1 c= the_Tree_of g ) by A17, A18, Th31, XTUPLE_0:def 12;
hence x in the_Tree_of g ; :: thesis: verum

end;

A19: S₂[f]

proof

let g1 be ConwayGame; :: thesis: ( g1 in dom f implies f . g1 = F₁(g1,(f | (the_proper_Tree_of g1))) )
assume g1 in dom f ; :: thesis: f . g1 = F₁(g1,(f | (the_proper_Tree_of g1)))
then [g1,(f . g1)] in f by FUNCT_1:def 2;
then ex x being set st
( [g1,(f . g1)] in x & x in FUNCS ) by TARSKI:def 4;
then consider fO being Function such that
A20: ( [g1,(f . g1)] in fO & fO in FUNCS ) ;
ex x being object st
( x in the_Tree_of g & S₄[x,fO] ) by A9, A20;
then consider gO being ConwayGame such that
A21: ( gO in the_Tree_of g & dom fO = the_Tree_of gO & S₂[fO] ) ;
A22: fO | (the_proper_Tree_of g1) = f | (the_proper_Tree_of g1)

proof

now :: thesis: ( dom (fO | (the_proper_Tree_of g1)) = dom (f | (the_proper_Tree_of g1)) & ( for x being object st x in dom (fO | (the_proper_Tree_of g1)) holds
(fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x ) )

g1 in the_Tree_of gO by A20, A21, FUNCT_1:1;
then the_Tree_of g1 c= the_Tree_of gO by Th31;
then A23: the_proper_Tree_of g1 c= dom fO by A21;
dom fO c= dom f by A20, COMPUT_1:13;
then A24: ( dom (fO | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 & dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 ) by A23, RELAT_1:62, XBOOLE_1:1;
hence dom (fO | (the_proper_Tree_of g1)) = dom (f | (the_proper_Tree_of g1)) ; :: thesis: for x being object st x in dom (fO | (the_proper_Tree_of g1)) holds
(fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom (fO | (the_proper_Tree_of g1)) implies (fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x )
assume A25: x in dom (fO | (the_proper_Tree_of g1)) ; :: thesis: (fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x
then ( x in dom fO & x in dom (f | (the_proper_Tree_of g1)) ) by A24, RELAT_1:57;
then ( fO . x = f . x & (fO | (the_proper_Tree_of g1)) . x = fO . x & (f | (the_proper_Tree_of g1)) . x = f . x ) by A25, A20, COMPUT_1:13, FUNCT_1:47;
hence (fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x ; :: thesis: verum

end;

end;

hence fO | (the_proper_Tree_of g1) = f | (the_proper_Tree_of g1) ; :: thesis: verum

end;

g1 in the_Tree_of gO by A20, A21, FUNCT_1:1;
then ( fO . g1 = F₁(g1,(fO | (the_proper_Tree_of g1))) & fO . g1 = f . g1 ) by A21, A20, COMPUT_1:13;
hence f . g1 = F₁(g1,(f | (the_proper_Tree_of g1))) by A22; :: thesis: verum

end;

g in dom f

proof

assume A26: not g in dom f ; :: thesis: contradiction
set v = F₁(g,(f | (the_proper_Tree_of g)));
dom {[g,F₁(g,(f | (the_proper_Tree_of g)))]} = {g} by RELAT_1:9;
then {[g,F₁(g,(f | (the_proper_Tree_of g)))]} tolerates f by A26, PARTFUN1:56, ZFMISC_1:50;
then reconsider h = {[g,F₁(g,(f | (the_proper_Tree_of g)))]} \/ f as Function by PARTFUN1:51;
A27: dom h = (dom f) \/ (dom {[g,F₁(g,(f | (the_proper_Tree_of g)))]}) by XTUPLE_0:23;
then A28: dom h = (dom f) \/ {g} by RELAT_1:9;
A29: S₄[g,h]

proof

take g ; :: thesis: ( g = g & ex f being Function st
( h = f & dom f = the_Tree_of g & S₂[f] ) )
thus g = g ; :: thesis: ex f being Function st
( h = f & dom f = the_Tree_of g & S₂[f] )
take h ; :: thesis: ( h = h & dom h = the_Tree_of g & S₂[h] )
thus h = h ; :: thesis: ( dom h = the_Tree_of g & S₂[h] )

now :: thesis: ( ( for x being object st x in the_Tree_of g holds
x in dom h ) & ( for x being object st x in dom h holds
x in the_Tree_of g ) )

hereby :: thesis: for x being object st x in dom h holds
x in the_Tree_of g

let x be object ; :: thesis: ( x in the_Tree_of g implies b₁ in dom h )
assume x in the_Tree_of g ; :: thesis: b₁ in dom h
then A30: x in ({g} /\ (the_Tree_of g)) \/ ((the_Tree_of g) \ {g}) by XBOOLE_1:51;

per cases ( x in {g} /\ (the_Tree_of g) or x in the_proper_Tree_of g ) by A30, XBOOLE_0:def 3;

suppose x in {g} /\ (the_Tree_of g) ; :: thesis: b₁ in dom h

then ( x in {g} & {g} c= dom h ) by A28, XBOOLE_0:def 4, XBOOLE_1:7;
hence x in dom h ; :: thesis: verum

end;

suppose x in the_proper_Tree_of g ; :: thesis: b₁ in dom h

then ( x in dom f & dom f c= dom h ) by A13, A27, XBOOLE_1:7;
hence x in dom h ; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom h implies b₁ in the_Tree_of g )
assume A31: x in dom h ; :: thesis: b₁ in the_Tree_of g

per cases ( x = g or x in dom f ) by A31, A28, ZFMISC_1:136;

suppose x = g ; :: thesis: b₁ in the_Tree_of g

hence x in the_Tree_of g by Th24; :: thesis: verum

end;

suppose x in dom f ; :: thesis: b₁ in the_Tree_of g

hence x in the_Tree_of g by A16; :: thesis: verum

end;

end;

end;

end;

hence A32: dom h = the_Tree_of g by TARSKI:2; :: thesis: S₂[h]
thus S₂[h] :: thesis: verum

proof

let g1 be ConwayGame; :: thesis: ( g1 in dom h implies h . g1 = F₁(g1,(h | (the_proper_Tree_of g1))) )
assume A33: g1 in dom h ; :: thesis: h . g1 = F₁(g1,(h | (the_proper_Tree_of g1)))

now :: thesis: ( f | (the_proper_Tree_of g1) c= h | (the_proper_Tree_of g1) & dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 & dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 )

thus f | (the_proper_Tree_of g1) c= h | (the_proper_Tree_of g1) by RELAT_1:76, XBOOLE_1:7; :: thesis: ( dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 & dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 )
A34: the_proper_Tree_of g1 c= the_proper_Tree_of g by Th32, A32, A33;
then A35: the_proper_Tree_of g1 c= dom f by A13;
thus dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 by A34, A13, RELAT_1:62, XBOOLE_1:1; :: thesis: dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1
f c= h by XBOOLE_1:7;
then dom f c= dom h by RELAT_1:11;
hence dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 by A35, RELAT_1:62, XBOOLE_1:1; :: thesis: verum

end;

then A36: h | (the_proper_Tree_of g1) = f | (the_proper_Tree_of g1) by GRFUNC_1:3;

per cases ( g1 = g or g1 in dom f ) by A33, A28, ZFMISC_1:136;

suppose A37: g1 = g ; :: thesis: h . g1 = F₁(g1,(h | (the_proper_Tree_of g1)))

[g,F₁(g,(f | (the_proper_Tree_of g)))] in h by ZFMISC_1:136;
hence h . g1 = F₁(g1,(h | (the_proper_Tree_of g1))) by A36, A33, A37, FUNCT_1:def 2; :: thesis: verum

end;

suppose A38: g1 in dom f ; :: thesis: h . g1 = F₁(g1,(h | (the_proper_Tree_of g1)))

f c= h by XBOOLE_1:7;
then f . g1 = h . g1 by A38, GRFUNC_1:2;
hence h . g1 = F₁(g1,(h | (the_proper_Tree_of g1))) by A19, A38, A36; :: thesis: verum

end;

end;

end;

end;

g in the_Tree_of g by Th24;
then h in FUNCS by A9, A29;
then h c= f by ZFMISC_1:74;
hence contradiction by A26, A28, RELAT_1:11, ZFMISC_1:39; :: thesis: verum

end;

then A39: {g} c= dom f by ZFMISC_1:31;
the_Tree_of g = (the_proper_Tree_of g) \/ {g} by Th24, ZFMISC_1:116;
then the_Tree_of g c= dom f by A39, A13, XBOOLE_1:8;
hence dom f = the_Tree_of g by A16, XBOOLE_0:def 10; :: thesis: S₂[f]
thus S₂[f] by A19; :: thesis: verum

end;

for g being ConwayGame holds S₃[g] from CGAMES_1:sch 3(A7);
hence for g being ConwayGame ex f being Function st
( dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = F₁(g1,(f | (the_proper_Tree_of g1))) ) ) ; :: thesis: verum