let C1, C2 be set ; :: thesis: ( ( for o being object holds
( o in C1 iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) ) & ( for o being object holds
( o in C2 iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) ) implies C1 = C2 )
assume that
A19: for o being object holds
( o in C1 iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) and
A20: for o being object holds
( o in C2 iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) ; :: thesis: C1 = C2

now :: thesis: for o being object holds
( o in C1 iff o in C2 )

let o be object ; :: thesis: ( o in C1 iff o in C2 )
( o in C1 iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) by A19;
hence ( o in C1 iff o in C2 ) by A20; :: thesis: verum

end;

hence C1 = C2 by TARSKI:2; :: thesis: verum