deffunc H₂( 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 <> {} } #);
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 = H₂(g1,f | (the_proper_Tree_of g1)) ) ) from CGAMES_1:sch 6();
then consider f being Function such that
A1: ( dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = H₂(g1,f | (the_proper_Tree_of g1)) ) ) ;
take v = f . g; :: thesis: ex f being Function st
( dom f = the_Tree_of g & v = 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 <> {} } #) ) )
take f ; :: thesis: ( dom f = the_Tree_of g & v = 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 <> {} } #) ) )
thus dom f = the_Tree_of g by A1; :: thesis: ( v = 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 <> {} } #) ) )
thus f . g = v ; :: thesis: 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 <> {} } #)
let g1 be ConwayGame; :: thesis: ( g1 in dom f implies 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 <> {} } #) )
assume A2: g1 in dom f ; :: thesis: 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 <> {} } #)
( { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } = { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } & { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } = { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ) by Lm3;
hence 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 <> {} } #) by A1, A2; :: thesis: verum