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