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