let n, i be Nat; :: thesis: (~ ((tau i) |^ n)) . 0 = (In ((- i),INT.Ring)) |^ n
(~ ((tau i) |^ n)) . 0 = (In ((- i),INT.Ring)) |^ n

proof

defpred S₁[ Nat] means (~ ((tau i) |^ $1)) . 0 = (In ((- i),INT.Ring)) |^ $1;
A1: S₁[ 0 ]

proof

(tau i) |^ 0 = 1_ (Polynom-Ring INT.Ring) by BINOM:8
.= 1. (Polynom-Ring INT.Ring) ;
then A2: ~ ((tau i) |^ 0) = 1_. INT.Ring by POLYNOM3:def 10;
(In ((- i),INT.Ring)) |^ 0 = 1_ INT.Ring by BINOM:8
.= 1. INT.Ring ;
hence S₁[ 0 ] by A2, POLYNOM3:30; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: (tau i) |^ (k + 1) = ((tau i) |^ 1) * ((tau i) |^ k) by BINOM:10
.= (tau i) * ((tau i) |^ k) by BINOM:8 ;
set p1 = ~ (tau i);
set q1 = ~ ((tau i) |^ k);
consider r being FinSequence of the carrier of INT.Ring such that
A7: ( len r = 0 + 1 & ((~ (tau i)) *' (~ ((tau i) |^ k))) . 0 = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = ((~ (tau i)) . (k -' 1)) * ((~ ((tau i) |^ k)) . ((0 + 1) -' k)) ) ) by POLYNOM3:def 9;
A8: r = <*(r . 1)*> by A7, FINSEQ_1:40;
dom r = Seg 1 by A7, FINSEQ_1:def 3;
then 1 in dom r ;
then A9: r . 1 = ((~ (tau i)) . (1 -' 1)) * ((~ ((tau i) |^ k)) . ((0 + 1) -' 1)) by A7
.= (In ((- i),INT.Ring)) * ((In ((- i),INT.Ring)) |^ k) by A4, POLYNOM5:38
.= ((In ((- i),INT.Ring)) |^ 1) * ((In ((- i),INT.Ring)) |^ k) by BINOM:8
.= (In ((- i),INT.Ring)) |^ (k + 1) by BINOM:10 ;
(~ ((tau i) |^ (k + 1))) . 0 = Sum r by A7, A5, POLYNOM3:def 10
.= (In ((- i),INT.Ring)) |^ (k + 1) by A8, A9, RLVECT_1:44 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence (~ ((tau i) |^ n)) . 0 = (In ((- i),INT.Ring)) |^ n ; :: thesis: verum

end;

hence (~ ((tau i) |^ n)) . 0 = (In ((- i),INT.Ring)) |^ n ; :: thesis: verum