let i be Integer; :: thesis: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K
for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a |^ i) = i * (v . a)
let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K
for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a |^ i) = i * (v . a)
let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a |^ i) = i * (v . a)
let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . (a |^ i) = i * (v . a) )
assume that
A1: K is having_valuation and
A2: a <> 0. K ; :: thesis: v . (a |^ i) = i * (v . a)
defpred S₁[ Nat] means v . (a |^ $1) = $1 * (v . a);
a |^ 0 = 1_ K by GROUP_1:def 7;
then A3: S₁[ 0 ] by A1, Th17;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: v . a in REAL by A1, A2, Th18, XXREAL_0:14;
reconsider N = n as ExtReal ;
thus v . (a |^ (n + 1)) = v . ((a |^ n) * a) by Lm2
.= (n * (v . a)) + (v . a) by A5, A1, Def8
.= (n * (v . a)) + (1. * (v . a)) by XXREAL_3:81
.= (v . a) * (N + 1.) by A6, XXREAL_3:95
.= (n + 1) * (v . a) by XXREAL_3:def 2 ; :: thesis: verum

end;

A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: v . (a |^ i) = i * (v . a)

then reconsider j = i as Element of NAT by INT_1:3;
S₁[j] by A7;
hence v . (a |^ i) = i * (v . a) ; :: thesis: verum

end;

suppose A8: i < 0 ; :: thesis: v . (a |^ i) = i * (v . a)

then reconsider n1 = - i as Element of NAT by INT_1:3;
reconsider I = i as ExtReal ;
A9: v . (a |^ i) = v . (((power K) . (a,|.i.|)) ") by A8, Def5
.= v . ((a |^ n1) ") by A8, ABSVALUE:def 1 ;
v . ((a |^ n1) ") = - (v . (a |^ n1)) by A1, A2, Th21, Lm3
.= - (n1 * (v . a)) by A7
.= - ((- I) * (v . a)) by XXREAL_3:def 3
.= - (- (i * (v . a))) by XXREAL_3:92 ;
hence v . (a |^ i) = i * (v . a) by A9; :: thesis: verum

end;

end;