deffunc H2( ConwayGame, Function) -> left-right = left-right(# { ($2 . gR) where gR is Element of the_RightOptions_of $1 : the_RightOptions_of $1 <> {} } , { ($2 . gL) where gL is Element of the_LeftOptions_of $1 : the_LeftOptions_of $1 <> {} } #);
let g1, g2 be set ; ( ex f being Function st
( dom f = the_Tree_of g & g1 = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) & ex f being Function st
( dom f = the_Tree_of g & g2 = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) implies g1 = g2 )
assume
ex f1 being Function st
( dom f1 = the_Tree_of g & g1 = f1 . g & ( for g0 being ConwayGame st g0 in dom f1 holds
f1 . g0 = H2(g0,f1) ) )
; ( for f being Function holds
( not dom f = the_Tree_of g or not g2 = f . g or ex g1 being ConwayGame st
( g1 in dom f & not f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) or g1 = g2 )
then consider f1 being Function such that
A3:
( dom f1 = the_Tree_of g & g1 = f1 . g & ( for g0 being ConwayGame st g0 in dom f1 holds
f1 . g0 = H2(g0,f1) ) )
;
assume
ex f2 being Function st
( dom f2 = the_Tree_of g & g2 = f2 . g & ( for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2) ) )
; g1 = g2
then consider f2 being Function such that
A4:
( dom f2 = the_Tree_of g & g2 = f2 . g & ( for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2) ) )
;
A5:
for g0 being ConwayGame st g0 in dom f1 holds
f1 . g0 = H2(g0,f1 | (the_proper_Tree_of g0))
A6:
for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0))
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 = H2(g1,f1 | (the_proper_Tree_of g1)) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = H2(g1,f2 | (the_proper_Tree_of g1)) ) holds
f1 = f2
from CGAMES_1:sch 5();
hence
g1 = g2
by A3, A4, A5, A6; verum