let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds

(normal-valuation v) . (Pgenerator v) = 1

let v be Valuation of K; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum

(normal-valuation v) . (Pgenerator v) = 1

let v be Valuation of K; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum