defpred S₁[ object , object ] means ( $1 is pair & L_ $1 is surreal & R_ $1 is surreal & ( for x1, y1 being Surreal st $1 = [x1,y1] holds
( 0_No < x1 & $2 = (1_No + ((x1 + (- x)) * y1)) * (x1 ") ) ) );
A1: for a, b, c being object st S₁[a,b] & S₁[a,c] holds
b = c

proof

let a, b, c be object ; :: thesis: ( S₁[a,b] & S₁[a,c] implies b = c )
assume A2: ( S₁[a,b] & S₁[a,c] ) ; :: thesis: b = c
consider a1, a2 being object such that
A3: a = [a1,a2] by XTUPLE_0:def 1, A2;
reconsider a1 = a1, a2 = a2 as Surreal by A3, A2;
thus b = (1_No + ((a1 + (- x)) * a2)) * (a1 ") by A3, A2
.= c by A3, A2 ; :: thesis: verum

end;

consider D being set such that
A4: for x being object holds
( x in D iff ex y being object st
( y in [:X,Y:] & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take D ; :: thesis: for o being object holds
( o in D iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) )
let o be object ; :: thesis: ( o in D iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) )
thus ( o in D implies ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) :: thesis: ( ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) implies o in D )

proof

assume o in D ; :: thesis: ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") )
then consider y being object such that
A5: ( y in [:X,Y:] & S₁[y,o] ) by A4;
consider a1, a2 being object such that
A6: y = [a1,a2] by XTUPLE_0:def 1, A5;
reconsider a1 = a1, a2 = a2 as Surreal by A6, A5;
take a1 ; :: thesis: ex y1 being Surreal st
( 0_No < a1 & a1 in X & y1 in Y & o = (1_No + ((a1 - x) * y1)) * (a1 ") )
take a2 ; :: thesis: ( 0_No < a1 & a1 in X & a2 in Y & o = (1_No + ((a1 - x) * a2)) * (a1 ") )
thus ( 0_No < a1 & a1 in X & a2 in Y & o = (1_No + ((a1 - x) * a2)) * (a1 ") ) by A6, A5, ZFMISC_1:87; :: thesis: verum

end;

given x1, y1 being Surreal such that A7: ( 0_No < x1 & x1 in X & y1 in Y ) and
A8: o = (1_No + ((x1 - x) * y1)) * (x1 ") ; :: thesis: o in D
A9: [x1,y1] in [:X,Y:] by A7, ZFMISC_1:87;
S₁[[x1,y1],o]

proof

thus ( [x1,y1] is pair & L_ [x1,y1] is surreal & R_ [x1,y1] is surreal ) ; :: thesis: for x1, y1 being Surreal st [x1,y1] = [x1,y1] holds
( 0_No < x1 & o = (1_No + ((x1 + (- x)) * y1)) * (x1 ") )
let X1, Y1 be Surreal; :: thesis: ( [x1,y1] = [X1,Y1] implies ( 0_No < X1 & o = (1_No + ((X1 + (- x)) * Y1)) * (X1 ") ) )
assume [x1,y1] = [X1,Y1] ; :: thesis: ( 0_No < X1 & o = (1_No + ((X1 + (- x)) * Y1)) * (X1 ") )
then ( x1 = X1 & y1 = Y1 ) by XTUPLE_0:1;
hence ( 0_No < X1 & o = (1_No + ((X1 + (- x)) * Y1)) * (X1 ") ) by A7, A8; :: thesis: verum

end;

hence o in D by A9, A4; :: thesis: verum