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 x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * ()

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * () )

assume A1: K is having_valuation ; :: thesis: for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * ()

let x be Element of K; :: thesis: ( x <> 0. K implies ex i being Integer st v . x = i * () )
assume A2: x <> 0. K ; :: thesis: ex i being Integer st v . x = i * ()
reconsider vx = v . x as Element of INT by A1, A2, Def8;
reconsider l = least-positive (rng v) as Integer by ;
A3: v . x = ((vx div l) * l) + (vx mod l) by INT_1:59;
per cases ( vx mod l = 0 or vx mod l <> 0 ) ;
suppose A4: vx mod l = 0 ; :: thesis: ex i being Integer st v . x = i * ()
take vx div l ; :: thesis: v . x = (vx div l) * ()
thus v . x = (vx div l) * () by ; :: thesis: verum
end;
suppose A5: vx mod l <> 0 ; :: thesis: ex i being Integer st v . x = i * ()
consider k being Element of K such that
A6: l = v . k by ;
set d = vx div l;
set kd = k |^ (vx div l);
set kD = (k |^ (vx div l)) " ;
A7: k <> 0. K by A1, A6, Def8;
then A8: (vx div l) * (v . k) = v . (k |^ (vx div l)) by ;
A9: - (v . (k |^ (vx div l))) = v . ((k |^ (vx div l)) ") by A1, A7, Th16, Th21;
A10: (vx div l) * l = (vx div l) * (v . k) by ;
A11: v . (x * ((k |^ (vx div l)) ")) = (v . x) - ((vx div l) * l) by A8, A9, A10, A1, Def8
.= vx - ((vx div l) * l) by Lm1
.= vx mod l by A3 ;
then A12: 0 <= v . (x * ((k |^ (vx div l)) ")) by INT_1:57;
A13: v . (x * ((k |^ (vx div l)) ")) < l by ;
v . (x * ((k |^ (vx div l)) ")) in rng v by FUNCT_2:4;
hence ex i being Integer st v . x = i * () by A12, A5, A11, A13, Def2; :: thesis: verum
end;
end;