let g be ConwayGame; :: thesis:
consider f being Function such that
A1: ( dom f = the_Tree_of g & f . g = - 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 <> {} } #) ) ) by Def14;
A2: for gO being ConwayGame st ( gO in the_RightOptions_of g or gO in the_LeftOptions_of g ) holds
f . gO = - gO

proof

let gO be ConwayGame; :: thesis:
assume ( gO in the_RightOptions_of g or gO in the_LeftOptions_of g ) ; :: thesis:
then ( gO in the_Options_of g & the_Options_of g c= the_Tree_of g ) by Th34, XBOOLE_0:def 3;
hence f . gO = - gO by Lm4, A1; :: thesis:

end;

set L = { (f . gR) where gR is Element of the_RightOptions_of g : the_RightOptions_of g <> {} } ;
set R = { (f . gL) where gL is Element of the_LeftOptions_of g : the_LeftOptions_of g <> {} } ;
- g = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g : the_RightOptions_of g <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g : the_LeftOptions_of g <> {} } #) by A1, Th24;
then A3: ( the_LeftOptions_of (- g) = { (f . gR) where gR is Element of the_RightOptions_of g : the_RightOptions_of g <> {} } & the_RightOptions_of (- g) = { (f . gL) where gL is Element of the_LeftOptions_of g : the_LeftOptions_of g <> {} } ) by Def6, Def7;

hereby :: thesis:

let x be set ; :: thesis:

hereby :: thesis:

assume x in the_LeftOptions_of (- g) ; :: thesis:
then consider gR0 being Element of the_RightOptions_of g such that
A4: ( x = f . gR0 & the_RightOptions_of g <> {} ) by A3;
reconsider gR = gR0 as ConwayGame by Th18, A4;
take gR = gR; :: thesis:
thus ( gR in the_RightOptions_of g & x = - gR ) by A4, A2; :: thesis:

end;

hereby :: thesis:

assume ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR ) ; :: thesis:
then consider gR being ConwayGame such that
A5: ( x = - gR & gR in the_RightOptions_of g ) ;
f . gR = - gR by A2, A5;
hence x in the_LeftOptions_of (- g) by A3, A5; :: thesis:

end;

end;

hereby :: thesis:

let x be set ; :: thesis:

hereby :: thesis:

assume x in the_RightOptions_of (- g) ; :: thesis:
then consider gL0 being Element of the_LeftOptions_of g such that
A6: ( x = f . gL0 & the_LeftOptions_of g <> {} ) by A3;
reconsider gL = gL0 as ConwayGame by Th18, A6;
take gL = gL; :: thesis:
thus ( gL in the_LeftOptions_of g & x = - gL ) by A6, A2; :: thesis:

end;

hereby :: thesis:

assume ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL ) ; :: thesis:
then consider gL being ConwayGame such that
A7: ( x = - gL & gL in the_LeftOptions_of g ) ;
f . gL = - gL by A2, A7;
hence x in the_RightOptions_of (- g) by A3, A7; :: thesis:

end;

end;