let g be ConwayGame; :: thesis: for f being Function st dom f = the_Tree_of 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 <> {} } #) ) holds
for g1 being ConwayGame st g1 in dom f holds
f . g1 = - g1
let f be Function; :: thesis: ( dom f = the_Tree_of 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 <> {} } #) ) implies for g1 being ConwayGame st g1 in dom f holds
f . g1 = - g1 )
assume A1: ( dom f = the_Tree_of 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 <> {} } #) ) ) ; :: thesis: for g1 being ConwayGame st g1 in dom f holds
f . g1 = - g1
let g1 be ConwayGame; :: thesis: ( g1 in dom f implies f . g1 = - g1 )
assume A2: g1 in dom f ; :: thesis: f . g1 = - g1
set f1 = f | (the_Tree_of g1);
A3: dom (f | (the_Tree_of g1)) = the_Tree_of g1 by A1, A2, Th31, RELAT_1:62;
now :: thesis: for g2 being ConwayGame st g2 in dom (f | (the_Tree_of g1)) holds
(f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #)
let g2 be ConwayGame; :: thesis: ( g2 in dom (f | (the_Tree_of g1)) implies (f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #) )
assume A4: g2 in dom (f | (the_Tree_of g1)) ; :: thesis: (f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #)
set L = { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ;
set L1 = { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ;
set R = { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ;
set R1 = { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ;
dom (f | (the_Tree_of g1)) c= dom f by RELAT_1:60;
then A5: f . g2 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #) by A1, A4;
A6: for gO being ConwayGame st ( gO in the_LeftOptions_of g2 or gO in the_RightOptions_of g2 ) holds
(f | (the_Tree_of g1)) . gO = f . gO
proof
let gO be ConwayGame; :: thesis: ( ( gO in the_LeftOptions_of g2 or gO in the_RightOptions_of g2 ) implies (f | (the_Tree_of g1)) . gO = f . gO )
assume ( gO in the_LeftOptions_of g2 or gO in the_RightOptions_of g2 ) ; :: thesis: (f | (the_Tree_of g1)) . gO = f . gO
then ( gO in the_Options_of g2 & the_Options_of g2 c= the_Tree_of g2 ) by Th34, XBOOLE_0:def 3;
then ( gO in the_Tree_of g2 & the_Tree_of g2 c= dom (f | (the_Tree_of g1)) ) by Th31, A4, A3;
hence (f | (the_Tree_of g1)) . gO = f . gO by FUNCT_1:47; :: thesis: verum
end;
now :: thesis: ( ( for x being object st x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } holds
x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ) & ( for x being object st x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } holds
x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ) )
hereby :: thesis: for x being object st x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } holds
x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} }
let x be object ; :: thesis: ( x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } implies x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } )
assume x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ; :: thesis: x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} }
then consider gR being Element of the_RightOptions_of g2 such that
A7: ( x = f . gR & the_RightOptions_of g2 <> {} ) ;
( gR in the_RightOptions_of g2 & gR is ConwayGame ) by A7, Th18;
then (f | (the_Tree_of g1)) . gR = f . gR by A6;
hence x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } by A7; :: thesis: verum
end;
hereby :: thesis: verum
let x be object ; :: thesis: ( x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } implies x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } )
assume x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ; :: thesis: x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} }
then consider gR being Element of the_RightOptions_of g2 such that
A8: ( x = (f | (the_Tree_of g1)) . gR & the_RightOptions_of g2 <> {} ) ;
( gR in the_RightOptions_of g2 & gR is ConwayGame ) by A8, Th18;
then (f | (the_Tree_of g1)) . gR = f . gR by A6;
hence x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } by A8; :: thesis: verum
end;
end;
then A9: { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } = { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } by TARSKI:2;
now :: thesis: ( ( for x being object st x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } holds
x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ) & ( for x being object st x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } holds
x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ) )
hereby :: thesis: for x being object st x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } holds
x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} }
let x be object ; :: thesis: ( x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } implies x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } )
assume x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ; :: thesis: x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} }
then consider gL being Element of the_LeftOptions_of g2 such that
A10: ( x = f . gL & the_LeftOptions_of g2 <> {} ) ;
( gL in the_LeftOptions_of g2 & gL is ConwayGame ) by A10, Th18;
then (f | (the_Tree_of g1)) . gL = f . gL by A6;
hence x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } by A10; :: thesis: verum
end;
hereby :: thesis: verum
let x be object ; :: thesis: ( x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } implies x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } )
assume x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ; :: thesis: x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} }
then consider gL being Element of the_LeftOptions_of g2 such that
A11: ( x = (f | (the_Tree_of g1)) . gL & the_LeftOptions_of g2 <> {} ) ;
( gL in the_LeftOptions_of g2 & gL is ConwayGame ) by A11, Th18;
then (f | (the_Tree_of g1)) . gL = f . gL by A6;
hence x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } by A11; :: thesis: verum
end;
end;
then { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } = { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } by TARSKI:2;
hence (f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #) by A4, A5, A9, FUNCT_1:47; :: thesis: verum
end;
then ( (f | (the_Tree_of g1)) . g1 = - g1 & g1 in dom (f | (the_Tree_of g1)) ) by Def14, A3, Th24;
hence f . g1 = - g1 by FUNCT_1:47; :: thesis: verum