let R be Ring; :: thesis: for a being Element of R
for n being Nat holds ((Frob R) `^ n) . a = a |^ ((Char R) |^ n)
let a be Element of R; :: thesis: for n being Nat holds ((Frob R) `^ n) . a = a |^ ((Char R) |^ n)
let n be Nat; :: thesis: ((Frob R) `^ n) . a = a |^ ((Char R) |^ n)
set p = Char R;
set f = Frob R;
defpred S<sub>1</sub>[ Nat] means ((Frob R) `^ $1) . a = a |^ ((Char R) |^ $1);
((Frob R) `^ 0) . a = (id R) . a by T1
.= a |^ 1 by BINOM:8
.= a |^ ((Char R) |^ 0) by NEWTON:4 ;
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]
((Frob R) `^ (k + 1)) . a = (((Frob R) `^ k) * (Frob R)) . a by T3
.= ((Frob R) * ((Frob R) `^ k)) . a by T3
.= (Frob R) . (a |^ ((Char R) |^ k)) by IV, FUNCT_2:15
.= (a |^ ((Char R) |^ k)) |^ (Char R) by defFr
.= a |^ (((Char R) |^ k) * (Char R)) by BINOM:11
.= a |^ ((Char R) |^ (k + 1)) by NEWTON:6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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