let g1 be ConwayGame; :: thesis: for f being Function holds
( { ((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 <> {} } )
let f be Function; :: thesis: ( { ((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 <> {} } )
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

proof

let gO be ConwayGame; :: thesis: ( ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) implies (f | (the_proper_Tree_of g1)) . gO = f . gO )
assume ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) ; :: thesis: (f | (the_proper_Tree_of g1)) . gO = f . gO
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: verum

end;

now :: thesis: ( ( for x being object st x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } holds
x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ) & ( for x being object st x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } holds
x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ) )

hereby :: thesis: for x being object st x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } holds
x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }

let x be object ; :: thesis: ( x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } implies x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } )
assume x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; :: thesis: x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
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: verum

end;

hereby :: thesis: verum

let x be object ; :: thesis: ( x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } implies x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } )
assume x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; :: thesis: x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
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: verum

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: { ((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 <> {} }

now :: thesis: ( ( for x being object st x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } holds
x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ) & ( for x being object st x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } holds
x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ) )

hereby :: thesis: for x being object st x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } holds
x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }

let x be object ; :: thesis: ( x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } implies x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } )
assume x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; :: thesis: x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }
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: verum

end;

hereby :: thesis: verum

let x be object ; :: thesis: ( x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } implies x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } )
assume x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; :: thesis: x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }
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: verum

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: verum