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 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 FUNCT_2:sch 4();
 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) / (least-positive (rng v)) 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 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;
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)) / (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
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;
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)) / (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 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)) / (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;
consider a being Element of K such that
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;
then reconsider f = f as 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