let g1 be ConwayGame; :: thesis:
let f be Function; :: thesis:
set R1 = { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ;
set R2 = { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ;
set L1 = { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ;
set L2 = { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ;
A1: for gO being ConwayGame st ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) holds
(f | (the_proper_Tree_of g1)) . gO = f . gO

let gO be ConwayGame; :: thesis:
assume ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) ; :: thesis:
then ( gO in the_Options_of g1 & the_Options_of g1 c= the_proper_Tree_of g1 ) by Th33, XBOOLE_0:def 3;
hence (f | (the_proper_Tree_of g1)) . gO = f . gO by FUNCT_1:49; :: thesis:

end;

hereby :: thesis:

let x be object ; :: thesis:
assume x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; :: thesis:
then consider gR being Element of the_RightOptions_of g1 such that
A2: ( x = (f | (the_proper_Tree_of g1)) . gR & the_RightOptions_of g1 <> {} ) ;
( gR in the_RightOptions_of g1 & gR is ConwayGame ) by A2, Th18;
then (f | (the_proper_Tree_of g1)) . gR = f . gR by A1;
hence x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } by A2; :: thesis:

end;

hereby :: thesis:

let x be object ; :: thesis:
assume x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; :: thesis:
then consider gR being Element of the_RightOptions_of g1 such that
A3: ( x = f . gR & the_RightOptions_of g1 <> {} ) ;
( gR in the_RightOptions_of g1 & gR is ConwayGame ) by A3, Th18;
then (f | (the_proper_Tree_of g1)) . gR = f . gR by A1;
hence x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } by A3; :: thesis:

end;

end;

hence { ((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 <> {} } by TARSKI:2; :: thesis:

hereby :: thesis:

let x be object ; :: thesis:
assume x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; :: thesis:
then consider gL being Element of the_LeftOptions_of g1 such that
A4: ( x = (f | (the_proper_Tree_of g1)) . gL & the_LeftOptions_of g1 <> {} ) ;
( gL in the_LeftOptions_of g1 & gL is ConwayGame ) by A4, Th18;
then (f | (the_proper_Tree_of g1)) . gL = f . gL by A1;
hence x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } by A4; :: thesis:

end;

hereby :: thesis:

let x be object ; :: thesis:
assume x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; :: thesis:
then consider gL being Element of the_LeftOptions_of g1 such that
A5: ( x = f . gL & the_LeftOptions_of g1 <> {} ) ;
( gL in the_LeftOptions_of g1 & gL is ConwayGame ) by A5, Th18;
then (f | (the_proper_Tree_of g1)) . gL = f . gL by A1;
hence x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } by A5; :: thesis:

end;

end;

hence { ((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 TARSKI:2; :: thesis: