let F be Field; :: thesis: for a being Element of F
for n being Nat holds (a | F) `^ n = (a |^ n) | F
let a be Element of F; :: thesis: for n being Nat holds (a | F) `^ n = (a |^ n) | F
let n be Nat; :: thesis: (a | F) `^ n = (a |^ n) | F
defpred S<sub>1</sub>[ Nat] means (a | F) `^ $1 = (a |^ $1) | F;
(a | F) `^ 0 = 1_. F by POLYNOM5:15
.= (1_ F) | F by RING_4:14
.= (a |^ 0) | F by BINOM:8 ;
then IA: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
(a | F) `^ (k + 1) = ((a |^ k) | F) *' (a | F) by IV, POLYNOM5:19
.= ((a |^ k) * a) | F by RING_4:18
.= ((a |^ k) * (a |^ 1)) | F by BINOM:8
.= (a |^ (k + 1)) | F by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence (a | F) `^ n = (a |^ n) | F ; :: thesis: verum