let i1, i2 be Function; :: thesis: ( dom i1 = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
i1 . y = inv y ) & dom i2 = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
i2 . y = inv y ) implies i1 = i2 )
assume that
A5: dom i1 = ((L_ x) \/ (R_ x)) \ {0_No} and
A6: for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
i1 . y = inv y and
A7: dom i2 = ((L_ x) \/ (R_ x)) \ {0_No} and
A8: for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
i2 . y = inv y ; :: thesis: i1 = i2
for o being object st o in ((L_ x) \/ (R_ x)) \ {0_No} holds
i1 . o = i2 . o

proof

let o be object ; :: thesis: ( o in ((L_ x) \/ (R_ x)) \ {0_No} implies i1 . o = i2 . o )
assume A9: o in ((L_ x) \/ (R_ x)) \ {0_No} ; :: thesis: i1 . o = i2 . o
then reconsider o = o as Surreal by SURREAL0:def 16;
i1 . o = inv o by A9, A6;
hence i1 . o = i2 . o by A9, A8; :: thesis: verum

end;

hence i1 = i2 by A5, A7, FUNCT_1:2; :: thesis: verum