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
for I being maximal Ideal of (ValuatRing v) holds I = vp v
let v be Valuation of K; :: thesis: ( K is having_valuation implies for I being maximal Ideal of (ValuatRing v) holds I = vp v )
assume A1: K is having_valuation ; :: thesis: for I being maximal Ideal of (ValuatRing v) holds I = vp v
let I be maximal Ideal of (ValuatRing v); :: thesis: I = vp v
assume A2: not I = vp v ; :: thesis: contradiction

per cases ( not I c= vp v or I c= vp v ) ;

suppose not I c= vp v ; :: thesis: contradiction

hence contradiction by A1, Th79; :: thesis: verum

end;

suppose I c= vp v ; :: thesis: contradiction

then ( not vp v is proper or I = vp v ) by RING_1:def 3;
then A3: ( vp v = the carrier of (ValuatRing v) or I = vp v ) ;
1. (ValuatRing v) = 1. K by A1, Def12;
hence contradiction by A3, A1, A2, Th63; :: thesis: verum

end;

end;