defpred S₁[ object , object ] means for y being Surreal st y = $1 holds
$2 = inv y;
A1: for e being object st e in ((L_ x) \/ (R_ x)) \ {0_No} holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in ((L_ x) \/ (R_ x)) \ {0_No} implies ex u being object st S₁[e,u] )
assume A2: e in ((L_ x) \/ (R_ x)) \ {0_No} ; :: thesis: ex u being object st S₁[e,u]
reconsider e = e as Surreal by A2, SURREAL0:def 16;
take inv e ; :: thesis: S₁[e, inv e]
thus S₁[e, inv e] ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = ((L_ x) \/ (R_ x)) \ {0_No} and
A4: for e being object st e in ((L_ x) \/ (R_ x)) \ {0_No} holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
take f ; :: thesis: ( dom f = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
f . y = inv y ) )
thus dom f = ((L_ x) \/ (R_ x)) \ {0_No} by A3; :: thesis: for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
f . y = inv y
let y be Surreal; :: thesis: ( y in ((L_ x) \/ (R_ x)) \ {0_No} implies f . y = inv y )
thus ( y in ((L_ x) \/ (R_ x)) \ {0_No} implies f . y = inv y ) by A4; :: thesis: verum