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 ;
A2: l1 in REAL by XREAL_0:def 1;
deffunc H1( 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 = H1(x) from for y being set st y in rng f holds
y is ext-integer
proof
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) / () by A3;
per cases ( v . x is integer or v . x = +infty ) by Def1;
suppose v . x is integer ; :: thesis: y is ext-integer
then x <> 0. K by ;
then consider r being Integer such that
A7: v . x = r * () by ;
(v . x) / () = r by ;
hence y is ext-integer by A5, A3; :: thesis: verum
end;
end;
end;
then reconsider f = f as e.i.-valued Function of K,ExtREAL by Def3;
f is Valuation of K
proof
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)) / () by A3
.= +infty / () by
.= +infty by ; :: 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
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 ;
then reconsider va = v . a as Integer ;
f . a = (v . a) / () by A3
.= va / l1 ;
hence f . a in INT by INT_1:def 2; :: thesis: verum
end;
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
0 <= f . ((1. K) + a) ) & ex a being Element of K st
( f . a <> 0 & f . a <> +infty ) )
proof
let a, b be Element of K; :: thesis: f . (a * b) = (f . a) + (f . b)
thus f . (a * b) = (v . (a * b)) / () by A3
.= ((v . a) + (v . b)) / () by
.= ((v . a) / ()) + ((v . b) / ()) by
.= (f . a) + ((v . b) / ()) by A3
.= (f . a) + (f . b) by A3 ; :: thesis: verum
end;
thus for a being Element of K st 0 <= f . a holds
0 <= f . ((1. K) + a) :: thesis: ex a being Element of K st
( f . a <> 0 & f . a <> +infty )
proof
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)) / () by A3;
f . a = (v . a) / () by A3;
then 0 <= v . a by A2, A8, Th5;
then 0 <= v . ((1. K) + a) by ;
hence 0 <= f . ((1. K) + a) by A9; :: thesis: verum
end;
consider a being Element of K such that
A10: v . a <> 0 and
A11: v . a <> +infty by ;
take a ; :: thesis: ( f . a <> 0 & f . a <> +infty )
A12: f . a = (v . a) / () by A3;
hence f . a <> 0 by A2, A10, Th9; :: thesis:
reconsider va = v . a as Integer by ;
A13: va in REAL by XREAL_0:def 1;
least-positive (rng v) in REAL by ;
hence f . a <> +infty by ; :: thesis: verum
end;
then reconsider f = f as Valuation of K ;
take f ; :: thesis: for a being Element of K holds v . a = (f . a) * ()
let a be Element of K; :: thesis: v . a = (f . a) * ()
thus v . a = ((v . a) / ()) * () by
.= (f . a) * () by A3 ; :: thesis: verum