let g be ConwayGame; :: thesis: for f1, f2 being Function st dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds
f1 . g1 = F₁(g1,(f1 | (the_proper_Tree_of g1))) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = F₁(g1,(f2 | (the_proper_Tree_of g1))) ) holds
f1 = f2
let f1, f2 be Function; :: thesis: ( dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds
f1 . g1 = F₁(g1,(f1 | (the_proper_Tree_of g1))) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = F₁(g1,(f2 | (the_proper_Tree_of g1))) ) implies f1 = f2 )
assume A1: ( dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds
f1 . g1 = F₁(g1,(f1 | (the_proper_Tree_of g1))) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = F₁(g1,(f2 | (the_proper_Tree_of g1))) ) ) ; :: thesis: f1 = f2
defpred S₂[ ConwayGame] means ( $1 in the_Tree_of g & f1 . $1 <> f2 . $1 );
assume f1 <> f2 ; :: thesis: contradiction
then ex x being object st
( x in the_Tree_of g & f1 . x <> f2 . x ) by A1;
then A2: ex g0 being ConwayGame st S₂[g0] ;
consider gm being ConwayGame such that
A3: ( S₂[gm] & ( for gO being ConwayGame st gO in the_proper_Tree_of gm holds
not S₂[gO] ) ) from CGAMES_1:sch 4(A2);
A4: f1 | (the_proper_Tree_of gm) = f2 | (the_proper_Tree_of gm)

proof

now :: thesis: ( dom (f1 | (the_proper_Tree_of gm)) = dom (f2 | (the_proper_Tree_of gm)) & ( for x being object st x in dom (f1 | (the_proper_Tree_of gm)) holds
(f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x ) )

set f1r = f1 | (the_proper_Tree_of gm);
set f2r = f2 | (the_proper_Tree_of gm);
A5: the_Tree_of gm c= the_Tree_of g by A3, Th31;
then A6: the_proper_Tree_of gm c= the_Tree_of g ;
A7: ( dom (f1 | (the_proper_Tree_of gm)) = the_proper_Tree_of gm & dom (f2 | (the_proper_Tree_of gm)) = the_proper_Tree_of gm ) by A1, A5, RELAT_1:62, XBOOLE_1:1;
hence dom (f1 | (the_proper_Tree_of gm)) = dom (f2 | (the_proper_Tree_of gm)) ; :: thesis: for x being object st x in dom (f1 | (the_proper_Tree_of gm)) holds
(f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom (f1 | (the_proper_Tree_of gm)) implies (f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x )
assume A8: x in dom (f1 | (the_proper_Tree_of gm)) ; :: thesis: (f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x
reconsider g0 = x as ConwayGame by A7, A8;
( f1 . x = f2 . x & (f1 | (the_proper_Tree_of gm)) . x = f1 . x & (f2 | (the_proper_Tree_of gm)) . x = f2 . x ) by A3, A6, A7, A8, FUNCT_1:47;
hence (f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x ; :: thesis: verum

end;

end;

hence f1 | (the_proper_Tree_of gm) = f2 | (the_proper_Tree_of gm) ; :: thesis: verum

end;

( f1 . gm = F₁(gm,(f1 | (the_proper_Tree_of gm))) & f2 . gm = F₁(gm,(f2 | (the_proper_Tree_of gm))) ) by A1, A3;
hence contradiction by A4, A3; :: thesis: verum