reconsider xx = x, yy = y as Surreal by A1;
let a1, a2 be Surreal; :: thesis: ( ( for x1, y1 being Surreal st x1 = x & y1 = y holds
a1 = x1 * y1 ) & ( for x1, y1 being Surreal st x1 = x & y1 = y holds
a2 = x1 * y1 ) implies a1 = a2 )
assume that
A2: for x1, y1 being Surreal st x1 = x & y1 = y holds
a1 = x1 * y1 and
A3: for x1, y1 being Surreal st x1 = x & y1 = y holds
a2 = x1 * y1 ; :: thesis: a1 = a2
a1 = xx * yy by A2;
hence a1 = a2 by A3; :: thesis: verum