defpred S₁[ object , object , object ] means ex n, m being Integer st
( c₁ = n & c₂ = m & c₃ = n + (<i> * m) );
A1: for x, y being object st x in INT & y in INT holds
ex z being object st
( z in G_INT_SET & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in INT & y in INT implies ex z being object st
( z in G_INT_SET & S₁[x,y,z] ) )
assume ( x in INT & y in INT ) ; :: thesis: ex z being object st
( z in G_INT_SET & S₁[x,y,z] )
then reconsider n = x, m = y as Integer ;
take n + (<i> * m) ; :: thesis: ( n + (<i> * m) in G_INT_SET & S₁[x,y,n + (<i> * m)] )
thus ( n + (<i> * m) in G_INT_SET & S₁[x,y,n + (<i> * m)] ) ; :: thesis: verum

end;

consider F being Function of [:INT,INT:],G_INT_SET such that
A2: for x, y being object st x in INT & y in INT holds
S₁[x,y,F . (x,y)] from BINOP_1:sch 1(A1);
A3: dom F = [:INT,INT:] by FUNCT_2:def 1;
A4: for n, m being Integer holds F . (n,m) = n + (<i> * m)

proof

let n, m be Integer; :: thesis: F . (n,m) = n + (<i> * m)
( n in INT & m in INT ) by INT_1:def 2;
then ex n1, m1 being Integer st
( n = n1 & m = m1 & F . (n,m) = n1 + (<i> * m1) ) by A2;
hence F . (n,m) = n + (<i> * m) ; :: thesis: verum

end;

now :: thesis: for x being object st x in G_INT_SET holds
x in rng F

let x be object ; :: thesis: ( x in G_INT_SET implies x in rng F )
assume x in G_INT_SET ; :: thesis: x in rng F
then reconsider x1 = x as G_INTEG by Th2;
A5: ( Re x1 in INT & Im x1 in INT ) by Def1;
reconsider n = Re x1, m = Im x1 as Integer ;
A6: F . (n,m) = n + (<i> * m) by A4
.= x1 by COMPLEX1:13 ;
[n,m] in [:INT,INT:] by A5, ZFMISC_1:87;
hence x in rng F by A3, A6, FUNCT_1:3; :: thesis: verum

end;

then A7: G_INT_SET c= rng F ;
F in Funcs ([:INT,INT:],G_INT_SET) by FUNCT_2:8;
then ex f being Function st
( F = f & dom f = [:INT,INT:] & rng f c= G_INT_SET ) by FUNCT_2:def 2;
then A8: rng F = G_INT_SET by A7, XBOOLE_0:def 10;
for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A9: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2
then consider n1, m1 being object such that
A10: ( n1 in INT & m1 in INT & x1 = [n1,m1] ) by A3, ZFMISC_1:def 2;
consider n2, m2 being object such that
A11: ( n2 in INT & m2 in INT & x2 = [n2,m2] ) by A9, A3, ZFMISC_1:def 2;
reconsider n1 = n1, m1 = m1, n2 = n2, m2 = m2 as Integer by A10, A11;
A12: F . x1 = F . (n1,m1) by A10
.= n1 + (<i> * m1) by A4 ;
A13: F . x2 = F . (n2,m2) by A11
.= n2 + (<i> * m2) by A4 ;
A14: n1 = Re (n2 + (<i> * m2)) by A9, A12, A13, COMPLEX1:12
.= n2 by COMPLEX1:12 ;
m1 = Im (n2 + (<i> * m2)) by A9, A12, A13, COMPLEX1:12
.= m2 by COMPLEX1:12 ;
hence x1 = x2 by A10, A11, A14; :: thesis: verum

end;

then [:INT,INT:], G_INT_SET are_equipotent by A8, A3, FUNCT_1:def 4, WELLORD2:def 4;
then A15: card [:INT,INT:] = card G_INT_SET by CARD_1:5;
( [:INT,INT:] is infinite & [:INT,INT:] is countable ) by CARD_4:7;
then card [:INT,INT:] = omega by CARD_3:def 15;
hence G_INT_SET is denumerable by CARD_3:def 15, A15; :: thesis: verum