deffunc H_{1}( Element of INT ) -> Element of LiouvilleNumbers = In ((c_{1} + Liouville_constant),LiouvilleNumbers);

consider f being Function of INT,LiouvilleNumbers such that

A1: for i being Element of INT holds f . i = H_{1}(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

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

consider f being Function of INT,LiouvilleNumbers such that

A1: for i being Element of INT holds f . i = H

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

then
f is one-to-one
by FUNCT_2:19;
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;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

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