deffunc H1( Element of INT ) -> Element of LiouvilleNumbers = In ((c1 + Liouville_constant),LiouvilleNumbers);
consider f being Function of INT,LiouvilleNumbers such that
A1: for i being Element of INT holds f . i = H1(i) from FUNCT_2:sch 4();
 A2: dom f = INT by FUNCT_2:def 1;
A3: rng f c= LiouvilleNumbers by RELAT_1:def 19;
for x1, x2 being object st x1 in INT & x2 in INT & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in INT & x2 in INT & f . x1 = f . x2 implies x1 = x2 )
assume ( x1 in INT & x2 in INT ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then reconsider xx1 = x1, xx2 = x2 as Element of INT ;
assume A4: f . x1 = f . x2 ; :: thesis: x1 = x2
A5: ( xx1 + Liouville_constant in LiouvilleNumbers & xx2 + Liouville_constant in LiouvilleNumbers ) ;
A6: f . x1 = In ((xx1 + Liouville_constant),LiouvilleNumbers) by A1
.= xx1 + Liouville_constant by A5, SUBSET_1:def 8 ;
f . x2 = In ((xx2 + Liouville_constant),LiouvilleNumbers) by A1
.= xx2 + Liouville_constant by A5, SUBSET_1:def 8 ;
hence x1 = x2 by A4, A6; :: thesis: verum
end;
then f is one-to-one by FUNCT_2:19;
then omega c= card LiouvilleNumbers by TOPGEN_3:16, A2, A3, CARD_1:10;
hence not LiouvilleNumbers is finite by FINSET_1:1; :: thesis: verum