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 ; :: thesis: ( 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) ) ) ; :: thesis: ( 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) ) ) ; :: thesis: 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))
proof
let g0 be ConwayGame; :: thesis: ( g0 in dom f1 implies f1 . g0 = H2(g0,f1 | (the_proper_Tree_of g0)) )
set LOr = { ((f1 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROr = { ((f1 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
set LOu = { (f1 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROu = { (f1 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
( { (f1 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } = { ((f1 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } & { (f1 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } = { ((f1 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ) by Lm3;
hence ( g0 in dom f1 implies f1 . g0 = H2(g0,f1 | (the_proper_Tree_of g0)) ) by A3; :: thesis: verum
end;
A6: for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0))
proof
let g0 be ConwayGame; :: thesis: ( g0 in dom f2 implies f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0)) )
set LOr = { ((f2 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROr = { ((f2 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
set LOu = { (f2 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROu = { (f2 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
( { (f2 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } = { ((f2 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } & { (f2 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } = { ((f2 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ) by Lm3;
hence ( g0 in dom f2 implies f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0)) ) by A4; :: thesis: verum
end;
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; :: thesis: verum