set A = { n where n is 3 -gonal Nat : n is 5 -gonal } ;
set B = { [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } ;
defpred S₁[ object , object ] means ex n being positive Nat st
( n = $1 `1 & $2 = Polygon (3,n) );
A1: for e being object st e in { [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in { [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } implies ex u being object st S₁[e,u] )
assume e in { [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } ; :: thesis: ex u being object st S₁[e,u]
then consider x, y being positive Nat such that
A2: e = [x,y] and
(y * ((3 * y) - 1)) - (x * (x + 1)) = 0 ;
take u = Polygon (3,x); :: thesis: S₁[e,u]
take n = x; :: thesis: ( n = e `1 & u = Polygon (3,n) )
thus n = e `1 by A2; :: thesis: u = Polygon (3,n)
thus u = Polygon (3,n) ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = { [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } and
A4: for e being object st e in { [x,y] where x, y is positive Nat : (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 } holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
A5: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f . x1 = f . x2 ; :: thesis: x1 = x2
consider n1 being positive Nat such that
A9: n1 = x1 `1 and
A10: f . x1 = Polygon (3,n1) by A3, A4, A6;
consider n2 being positive Nat such that
A11: ( n2 = x2 `1 & f . x2 = Polygon (3,n2) ) by A3, A4, A7;
consider c1, d1 being positive Nat such that
A12: x1 = [c1,d1] and
A13: (d1 * ((3 * d1) - 1)) - (c1 * (c1 + 1)) = 0 by A3, A6;
consider c2, d2 being positive Nat such that
A14: x2 = [c2,d2] and
A15: (d2 * ((3 * d2) - 1)) - (c2 * (c2 + 1)) = 0 by A3, A7;
A16: 3 * ((d1 * d1) - (d2 * d2)) = d1 - d2 by A8, A9, A10, A11, A12, A13, A14, A15;

now :: thesis: not d1 <> d2

assume d1 <> d2 ; :: thesis: contradiction

per cases then ( d1 < d2 or d2 < d1 ) by XXREAL_0:1;

suppose d1 < d2 ; :: thesis: contradiction

then consider z being positive Nat such that
A17: d2 = d1 + z by Th1;
3 * ((d1 * d1) - ((d1 + z) * (d1 + z))) = (d1 - d1) - z by A16, A17;
then (3 * ((2 * d1) + z)) * z = 1 * z ;
then 3 * ((2 * d1) + z) = 1 by XCMPLX_1:5;
hence contradiction by Lm20; :: thesis: verum

end;

suppose d2 < d1 ; :: thesis: contradiction

then consider z being positive Nat such that
A18: d1 = d2 + z by Th1;
(3 * ((2 * d2) + z)) * z = 1 * z by A16, A18;
then 3 * ((2 * d2) + z) = 1 by XCMPLX_1:5;
hence contradiction by Lm20; :: thesis: verum

end;

end;

end;

hence x1 = x2 by A8, A9, A10, A11, A12, A14, Th67; :: thesis: verum

end;

rng f c= { n where n is 3 -gonal Nat : n is 5 -gonal }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng f or t in { n where n is 3 -gonal Nat : n is 5 -gonal } )
assume t in rng f ; :: thesis: t in { n where n is 3 -gonal Nat : n is 5 -gonal }
then consider s being object such that
A19: s in dom f and
A20: f . s = t by FUNCT_1:def 3;
consider x, y being positive Nat such that
A21: ( s = [x,y] & (y * ((3 * y) - 1)) - (x * (x + 1)) = 0 ) by A3, A19;
A22: S₁[s,f . s] by A3, A4, A19;
then f . s = Polygon (5,y) by A21;
hence t in { n where n is 3 -gonal Nat : n is 5 -gonal } by A20, A22; :: thesis: verum

end;

hence { n where n is 3 -gonal Nat : n is 5 -gonal } is infinite by A3, A5, Th68, CARD_1:59; :: thesis: verum