let n be Nat; for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
let v be Valuation of K; ( K is having_valuation implies for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n) )
set R = ValuatRing v;
assume A1:
K is having_valuation
; for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
let y be Element of (ValuatRing v); (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
defpred S1[ Nat] means (power K) . (y,$1) = (power (ValuatRing v)) . (y,$1);
reconsider x = y as Element of K by A1, Th51;
( (power K) . (x,0) = 1_ K & (power (ValuatRing v)) . (y,0) = 1_ (ValuatRing v) )
by GROUP_1:def 7;
then A2:
S1[ 0 ]
by A1, Def12;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
(power K) . (y,n) = (power (ValuatRing v)) . (y,n)
; verum