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 () holds () . (y,n) = (power ()) . (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 () holds () . (y,n) = (power ()) . (y,n)

let v be Valuation of K; :: thesis: ( K is having_valuation implies for y being Element of () holds () . (y,n) = (power ()) . (y,n) )
set R = ValuatRing v;
assume A1: K is having_valuation ; :: thesis: for y being Element of () holds () . (y,n) = (power ()) . (y,n)
let y be Element of (); :: thesis: () . (y,n) = (power ()) . (y,n)
defpred S1[ Nat] means () . (y,\$1) = (power ()) . (y,\$1);
reconsider x = y as Element of K by ;
( (power K) . (x,0) = 1_ K & (power ()) . (y,0) = 1_ () ) by GROUP_1:def 7;
then A2: S1[ 0 ] by ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
reconsider m = n as Element of NAT by ORDINAL1:def 12;
( (power K) . (y,(n + 1)) = (() . (x,m)) * x & (power ()) . (y,(n + 1)) = ((power ()) . (y,m)) * y ) by GROUP_1:def 7;
hence S1[n + 1] by A1, A4, Th55; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A2, A3);
hence (power K) . (y,n) = (power ()) . (y,n) ; :: thesis: verum