let F be Field; :: thesis: for a being non zero Element of F
for n being Nat holds (a ") |^ n = (a |^ n) "
let a be non zero Element of F; :: thesis: for n being Nat holds (a ") |^ n = (a |^ n) "
let n be Nat; :: thesis: (a ") |^ n = (a |^ n) "
defpred S₁[ Nat] means (a ") |^ $1 = (a |^ $1) " ;
(a ") |^ 0 = (1_ F) " by BINOM:8
.= (a |^ 0) " 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: ( a <> 0. F & a |^ k <> 0. F ) ;
(a ") |^ (k + 1) = ((a ") |^ k) * ((a ") |^ 1) by BINOM:10
.= ((a ") |^ k) * (a ") by BINOM:8
.= (a * (a |^ k)) " by IV, A, VECTSP_2:11
.= ((a |^ k) * (a |^ 1)) " by BINOM:8
.= (a |^ (k + 1)) " 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 ") |^ n = (a |^ n) " ; :: thesis: verum