consider f being Function such that
A1: ( dom f = the_Tree_of g & - g = 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 <> {} } #) ) ) by Def14;
defpred S₂[ ConwayGame] means ( g in dom f implies f . g is ConwayGame );
A2: for g1 being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g1 holds
S₂[gO] ) holds
S₂[g1]

proof

let g1 be ConwayGame; :: thesis: ( ( for gO being ConwayGame st gO in the_Options_of g1 holds
S₂[gO] ) implies S₂[g1] )
assume A3: for gO being ConwayGame st gO in the_Options_of g1 holds
S₂[gO] ; :: thesis: S₂[g1]
assume A4: g1 in dom f ; :: thesis: f . g1 is ConwayGame
set L = { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ;
set R = { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ;
A5: 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, A4;

now :: thesis: for z being set st z in { (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 <> {} } holds
z is ConwayGame

let z be set ; :: thesis: ( z in { (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 z is ConwayGame )
assume A6: z in { (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 <> {} } ; :: thesis: z is ConwayGame
ex gO being ConwayGame st
( gO in the_Options_of g1 & z = f . gO )

proof

per cases ( z in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } or z in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ) by A6, XBOOLE_0:def 3;

suppose z in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; :: thesis: ex gO being ConwayGame st
( gO in the_Options_of g1 & z = f . gO )

then consider gR being Element of the_RightOptions_of g1 such that
A7: ( z = f . gR & the_RightOptions_of g1 <> {} ) ;
reconsider gO = gR as ConwayGame by Th18, A7;
take gO ; :: thesis: ( gO in the_Options_of g1 & z = f . gO )
thus ( gO in the_Options_of g1 & z = f . gO ) by A7, XBOOLE_0:def 3; :: thesis: verum

end;

suppose z in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; :: thesis: ex gO being ConwayGame st
( gO in the_Options_of g1 & z = f . gO )

then consider gL being Element of the_LeftOptions_of g1 such that
A8: ( z = f . gL & the_LeftOptions_of g1 <> {} ) ;
reconsider gO = gL as ConwayGame by Th18, A8;
take gO ; :: thesis: ( gO in the_Options_of g1 & z = f . gO )
thus ( gO in the_Options_of g1 & z = f . gO ) by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then consider gO being ConwayGame such that
A9: ( gO in the_Options_of g1 & z = f . gO ) ;
( the_Options_of g1 c= the_Tree_of g1 & the_Tree_of g1 c= dom f ) by Th34, Th31, A4, A1;
then the_Options_of g1 c= dom f ;
hence z is ConwayGame by A3, A9; :: thesis: verum

end;

hence f . g1 is ConwayGame by A5, Th19; :: thesis: verum

end;

A10: for g being ConwayGame holds S₂[g] from CGAMES_1:sch 3(A2);
g in the_Tree_of g by Th24;
hence - g is ConwayGame-like by A1, A10; :: thesis: verum