let D1, D2 be surreal-membered set ; :: thesis: ( ( for o being object holds
( o in D1 iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) ) ) & ( for o being object holds
( o in D2 iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) ) ) implies D1 = D2 )
assume that
A2: for o being object holds
( o in D1 iff ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) and
A3: for o being object holds
( o in D2 iff ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) ; :: thesis: D1 = D2

now :: thesis: for o being object holds
( o in D1 iff o in D2 )

let o be object ; :: thesis: ( o in D1 iff o in D2 )
( o in D1 iff ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) by A2;
hence ( o in D1 iff o in D2 ) by A3; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum