let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)

let y be Element of (ValuatRing v); :: thesis: (power K) . (y,n) = (power (ValuatRing v)) . (y,n)

defpred S_{1}[ 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: S_{1}[ 0 ]
by A1, Def12;

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A2, A3);

hence (power K) . (y,n) = (power (ValuatRing v)) . (y,n) ; :: thesis: verum

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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)

let y be Element of (ValuatRing v); :: thesis: (power K) . (y,n) = (power (ValuatRing v)) . (y,n)

defpred S

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: S

A3: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

reconsider m = n as Element of NAT by ORDINAL1:def 12;

( (power K) . (y,(n + 1)) = ((power K) . (x,m)) * x & (power (ValuatRing v)) . (y,(n + 1)) = ((power (ValuatRing v)) . (y,m)) * y ) by GROUP_1:def 7;

hence S_{1}[n + 1]
by A1, A4, Th55; :: thesis: verum

end;assume A4: S

reconsider m = n as Element of NAT by ORDINAL1:def 12;

( (power K) . (y,(n + 1)) = ((power K) . (x,m)) * x & (power (ValuatRing v)) . (y,(n + 1)) = ((power (ValuatRing v)) . (y,m)) * y ) by GROUP_1:def 7;

hence S

hence (power K) . (y,n) = (power (ValuatRing v)) . (y,n) ; :: thesis: verum