set l = least-positive (rng v);

reconsider ll = least-positive (rng v) as Element of ExtREAL by XXREAL_0:def 1;

reconsider l1 = least-positive (rng v) as Integer by A1, Th35;

A2: l1 in REAL by XREAL_0:def 1;

deffunc H_{1}( Element of K) -> Element of ExtREAL = (v . $1) / ll;

consider f being Function of K,ExtREAL such that

A3: for x being Element of K holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

for y being set st y in rng f holds

y is ext-integer

f is Valuation of K

take f ; :: thesis: for a being Element of K holds v . a = (f . a) * (least-positive (rng v))

let a be Element of K; :: thesis: v . a = (f . a) * (least-positive (rng v))

thus v . a = ((v . a) / (least-positive (rng v))) * (least-positive (rng v)) by A2, Th8

.= (f . a) * (least-positive (rng v)) by A3 ; :: thesis: verum

reconsider ll = least-positive (rng v) as Element of ExtREAL by XXREAL_0:def 1;

reconsider l1 = least-positive (rng v) as Integer by A1, Th35;

A2: l1 in REAL by XREAL_0:def 1;

deffunc H

consider f being Function of K,ExtREAL such that

A3: for x being Element of K holds f . x = H

for y being set st y in rng f holds

y is ext-integer

proof

then reconsider f = f as e.i.-valued Function of K,ExtREAL by Def3;
let y be set ; :: thesis: ( y in rng f implies y is ext-integer )

assume y in rng f ; :: thesis: y is ext-integer

then consider x being object such that

A4: x in dom f and

A5: f . x = y by FUNCT_1:def 3;

reconsider x = x as Element of K by A4;

A6: f . x = (v . x) / (least-positive (rng v)) by A3;

end;assume y in rng f ; :: thesis: y is ext-integer

then consider x being object such that

A4: x in dom f and

A5: f . x = y by FUNCT_1:def 3;

reconsider x = x as Element of K by A4;

A6: f . x = (v . x) / (least-positive (rng v)) by A3;

per cases
( v . x is integer or v . x = +infty )
by Def1;

end;

suppose
v . x is integer
; :: thesis: y is ext-integer

then
x <> 0. K
by A1, Def8;

then consider r being Integer such that

A7: v . x = r * (least-positive (rng v)) by A1, Th36;

(v . x) / (least-positive (rng v)) = r by A2, A7, XXREAL_3:88;

hence y is ext-integer by A5, A3; :: thesis: verum

end;then consider r being Integer such that

A7: v . x = r * (least-positive (rng v)) by A1, Th36;

(v . x) / (least-positive (rng v)) = r by A2, A7, XXREAL_3:88;

hence y is ext-integer by A5, A3; :: thesis: verum

f is Valuation of K

proof

then reconsider f = f as Valuation of K ;
thus
K is having_valuation
by A1; :: according to FVALUAT1:def 8 :: thesis: ( f . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds

f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

thus f . (0. K) = (v . (0. K)) / (least-positive (rng v)) by A3

.= +infty / (least-positive (rng v)) by A1, Def8

.= +infty by A2, XXREAL_3:83 ; :: thesis: ( ( for a being Element of K st a <> 0. K holds

f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

thus for a being Element of K st a <> 0. K holds

f . a in INT :: thesis: ( ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

0 <= f . ((1. K) + a) :: thesis: ex a being Element of K st

( f . a <> 0 & f . a <> +infty )

A10: v . a <> 0 and

A11: v . a <> +infty by A1, Def8;

take a ; :: thesis: ( f . a <> 0 & f . a <> +infty )

A12: f . a = (v . a) / (least-positive (rng v)) by A3;

hence f . a <> 0 by A2, A10, Th9; :: thesis: f . a <> +infty

reconsider va = v . a as Integer by A11, Def1;

A13: va in REAL by XREAL_0:def 1;

least-positive (rng v) in REAL by A1, Lm6;

hence f . a <> +infty by A12, A13; :: thesis: verum

end;f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

thus f . (0. K) = (v . (0. K)) / (least-positive (rng v)) by A3

.= +infty / (least-positive (rng v)) by A1, Def8

.= +infty by A2, XXREAL_3:83 ; :: thesis: ( ( for a being Element of K st a <> 0. K holds

f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

thus for a being Element of K st a <> 0. K holds

f . a in INT :: thesis: ( ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

proof

thus
for a, b being Element of K holds f . (a * b) = (f . a) + (f . b)
:: thesis: ( ( for a being Element of K st 0 <= f . a holds
let a be Element of K; :: thesis: ( a <> 0. K implies f . a in INT )

assume a <> 0. K ; :: thesis: f . a in INT

then v . a in INT by A1, Def8;

then reconsider va = v . a as Integer ;

f . a = (v . a) / (least-positive (rng v)) by A3

.= va / l1 ;

hence f . a in INT by INT_1:def 2; :: thesis: verum

end;assume a <> 0. K ; :: thesis: f . a in INT

then v . a in INT by A1, Def8;

then reconsider va = v . a as Integer ;

f . a = (v . a) / (least-positive (rng v)) by A3

.= va / l1 ;

hence f . a in INT by INT_1:def 2; :: thesis: verum

0 <= f . ((1. K) + a) ) & ex a being Element of K st

( f . a <> 0 & f . a <> +infty ) )

proof

thus
for a being Element of K st 0 <= f . a holds
let a, b be Element of K; :: thesis: f . (a * b) = (f . a) + (f . b)

thus f . (a * b) = (v . (a * b)) / (least-positive (rng v)) by A3

.= ((v . a) + (v . b)) / (least-positive (rng v)) by A1, Def8

.= ((v . a) / (least-positive (rng v))) + ((v . b) / (least-positive (rng v))) by A2, Th7

.= (f . a) + ((v . b) / (least-positive (rng v))) by A3

.= (f . a) + (f . b) by A3 ; :: thesis: verum

end;thus f . (a * b) = (v . (a * b)) / (least-positive (rng v)) by A3

.= ((v . a) + (v . b)) / (least-positive (rng v)) by A1, Def8

.= ((v . a) / (least-positive (rng v))) + ((v . b) / (least-positive (rng v))) by A2, Th7

.= (f . a) + ((v . b) / (least-positive (rng v))) by A3

.= (f . a) + (f . b) by A3 ; :: thesis: verum

0 <= f . ((1. K) + a) :: thesis: ex a being Element of K st

( f . a <> 0 & f . a <> +infty )

proof

consider a being Element of K such that
let a be Element of K; :: thesis: ( 0 <= f . a implies 0 <= f . ((1. K) + a) )

assume A8: 0 <= f . a ; :: thesis: 0 <= f . ((1. K) + a)

A9: f . ((1. K) + a) = (v . ((1. K) + a)) / (least-positive (rng v)) by A3;

f . a = (v . a) / (least-positive (rng v)) by A3;

then 0 <= v . a by A2, A8, Th5;

then 0 <= v . ((1. K) + a) by A1, Def8;

hence 0 <= f . ((1. K) + a) by A9; :: thesis: verum

end;assume A8: 0 <= f . a ; :: thesis: 0 <= f . ((1. K) + a)

A9: f . ((1. K) + a) = (v . ((1. K) + a)) / (least-positive (rng v)) by A3;

f . a = (v . a) / (least-positive (rng v)) by A3;

then 0 <= v . a by A2, A8, Th5;

then 0 <= v . ((1. K) + a) by A1, Def8;

hence 0 <= f . ((1. K) + a) by A9; :: thesis: verum

A10: v . a <> 0 and

A11: v . a <> +infty by A1, Def8;

take a ; :: thesis: ( f . a <> 0 & f . a <> +infty )

A12: f . a = (v . a) / (least-positive (rng v)) by A3;

hence f . a <> 0 by A2, A10, Th9; :: thesis: f . a <> +infty

reconsider va = v . a as Integer by A11, Def1;

A13: va in REAL by XREAL_0:def 1;

least-positive (rng v) in REAL by A1, Lm6;

hence f . a <> +infty by A12, A13; :: thesis: verum

take f ; :: thesis: for a being Element of K holds v . a = (f . a) * (least-positive (rng v))

let a be Element of K; :: thesis: v . a = (f . a) * (least-positive (rng v))

thus v . a = ((v . a) / (least-positive (rng v))) * (least-positive (rng v)) by A2, Th8

.= (f . a) * (least-positive (rng v)) by A3 ; :: thesis: verum