defpred S₁[ object ] means $1 is surreal ;
consider X1 being set such that
A1: for o being object holds
( o in X1 iff ( o in X & S₁[o] ) ) from XBOOLE_0:sch 1();
consider Y1 being set such that
A2: for o being object holds
( o in Y1 iff ( o in Y & S₁[o] ) ) from XBOOLE_0:sch 1();
defpred S₂[ object , object ] means for a being Surreal st a = $1 holds
$2 = a * y;
defpred S₃[ object , object ] means for a being Surreal st a = $1 holds
$2 = x * a;
A3: for o being object st o in X1 holds
ex u being object st S₂[o,u]

let o be object ; :: thesis:
assume A4: o in X1 ; :: thesis:
reconsider a = o as Surreal by A4, A1;
take a * y ; :: thesis:
thus S₂[o,a * y] ; :: thesis:

end;

consider fy being Function such that
A5: ( dom fy = X1 & ( for o being object st o in X1 holds
S₂[o,fy . o] ) ) from CLASSES1:sch 1(A3);
A6: for o being object st o in Y1 holds
ex u being object st S₃[o,u]

let o be object ; :: thesis:
assume A7: o in Y1 ; :: thesis:
reconsider a = o as Surreal by A7, A2;
take x * a ; :: thesis:
thus S₃[o,x * a] ; :: thesis:

end;

consider fx being Function such that
A8: ( dom fx = Y1 & ( for o being object st o in Y1 holds
S₃[o,fx . o] ) ) from CLASSES1:sch 1(A6);
defpred S₄[ object , object ] means for a, b being Surreal st $1 = [a,b] holds
$2 = a * b;
A9: for o being object st o in [:X1,Y1:] holds
ex u being object st S₄[o,u]

let o be object ; :: thesis:
assume A10: o in [:X1,Y1:] ; :: thesis:
consider a, b being object such that
A11: ( a in X1 & b in Y1 & o = [a,b] ) by A10, ZFMISC_1:def 2;
reconsider a = a, b = b as Surreal by A11, A1, A2;
take a * b ; :: thesis:
let a1, b1 be Surreal; :: thesis:
assume o = [a1,b1] ; :: thesis:
then ( a1 = a & b1 = b ) by A11, XTUPLE_0:1;
hence a * b = a1 * b1 ; :: thesis:

end;

consider fxy being Function such that
A12: ( dom fxy = [:X1,Y1:] & ( for o being object st o in [:X1,Y1:] holds
S₄[o,fxy . o] ) ) from CLASSES1:sch 1(A9);
set IT = { (((fy . x1) +' (fx . y1)) +' (-' (fxy . [x1,y1]))) where x1 is Element of X, y1 is Element of Y : ( x1 in X & y1 in Y & x1 is surreal & y1 is surreal ) } ;
take { (((fy . x1) +' (fx . y1)) +' (-' (fxy . [x1,y1]))) where x1 is Element of X, y1 is Element of Y : ( x1 in X & y1 in Y & x1 is surreal & y1 is surreal ) } ; :: thesis:
let o be object ; :: thesis:
thus ( o in { (((fy . x1) +' (fx . y1)) +' (-' (fxy . [x1,y1]))) where x1 is Element of X, y1 is Element of Y : ( x1 in X & y1 in Y & x1 is surreal & y1 is surreal ) } implies ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) :: thesis:

assume o in { (((fy . x1) +' (fx . y1)) +' (-' (fxy . [x1,y1]))) where x1 is Element of X, y1 is Element of Y : ( x1 in X & y1 in Y & x1 is surreal & y1 is surreal ) } ; :: thesis:
then consider x1 being Element of X, y1 being Element of Y such that
A13: ( o = ((fy . x1) +' (fx . y1)) +' (-' (fxy . [x1,y1])) & x1 in X & y1 in Y & x1 is surreal & y1 is surreal ) ;
reconsider x1 = x1, y1 = y1 as Surreal by A13;
( x1 in X1 & y1 in Y1 ) by A13, A1, A2;
then [x1,y1] in [:X1,Y1:] by ZFMISC_1:def 2;
then A14: fxy . [x1,y1] = x1 * y1 by A12;
A15: fy . x1 = x1 * y by A13, A1, A5;
fx . y1 = x * y1 by A13, A2, A8;
hence ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by A13, A14, A15; :: thesis:

end;

given x1, y1 being Surreal such that A16: ( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ; :: thesis:
( x1 in X1 & y1 in Y1 ) by A16, A1, A2;
then [x1,y1] in [:X1,Y1:] by ZFMISC_1:def 2;
then A17: fxy . [x1,y1] = x1 * y1 by A12;
A18: fy . x1 = x1 * y by A16, A1, A5;
fx . y1 = x * y1 by A16, A2, A8;
hence o in { (((fy . x1) +' (fx . y1)) +' (-' (fxy . [x1,y1]))) where x1 is Element of X, y1 is Element of Y : ( x1 in X & y1 in Y & x1 is surreal & y1 is surreal ) } by A16, A17, A18; :: thesis: