let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
(normal-valuation v) . (Pgenerator v) = 1
let v be Valuation of K; ( K is having_valuation implies (normal-valuation v) . (Pgenerator v) = 1 )
set f = normal-valuation v;
set a = Pgenerator v;
set l = least-positive (rng v);
assume A1:
K is having_valuation
; (normal-valuation v) . (Pgenerator v) = 1
then A2:
v . (Pgenerator v) = ((normal-valuation v) . (Pgenerator v)) * (least-positive (rng v))
by Def10;
A3:
least-positive (rng v) in REAL
by A1, Lm6;
least-positive (rng v) in rng v
by A1, Lm5;
then
{(least-positive (rng v))} c= rng v
by ZFMISC_1:31;
then A4:
not v " {(least-positive (rng v))} is empty
by RELAT_1:139;
Pgenerator v = the Element of v " {(least-positive (rng v))}
by A1, Def9;
then
v . (Pgenerator v) in {(least-positive (rng v))}
by A4, FUNCT_1:def 7;
then v . (Pgenerator v) =
least-positive (rng v)
by TARSKI:def 1
.=
1 * (least-positive (rng v))
by XXREAL_3:81
;
hence
(normal-valuation v) . (Pgenerator v) = 1
by A2, A3, XXREAL_3:68; verum