let f, g be Valuation of K; :: thesis: ( ( for a being Element of K holds v . a = (f . a) * (least-positive (rng v)) ) & ( for a being Element of K holds v . a = (g . a) * (least-positive (rng v)) ) implies f = g )

assume that

A14: for a being Element of K holds v . a = (f . a) * (least-positive (rng v)) and

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

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

let x be Element of K; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x

(f . x) * (least-positive (rng v)) = v . x by A14

.= (g . x) * (least-positive (rng v)) by A15 ;

hence f . x = g . x by A16, XXREAL_3:68; :: thesis: verum

assume that

A14: for a being Element of K holds v . a = (f . a) * (least-positive (rng v)) and

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

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

let x be Element of K; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x

(f . x) * (least-positive (rng v)) = v . x by A14

.= (g . x) * (least-positive (rng v)) by A15 ;

hence f . x = g . x by A16, XXREAL_3:68; :: thesis: verum