let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: for n being non zero Nat
for i being Element of NAT holds
( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) )
let n be non zero Nat; :: thesis: for i being Element of NAT holds
( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) )
let i be Element of NAT ; :: thesis: ( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) )
( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) )

proof

defpred S₁[ Nat] means ( ((~ ((tau 0) |^ $1)) *' f) . (i + $1) = f . i & ((~ ((tau 0) |^ $1)) *' f) | (Segm $1) = (Segm $1) --> (0. INT.Ring) );
A1: (~ ((tau 0) |^ 1)) *' f = (tau 0) *' f by BINOM:8;
A2: ((~ ((tau 0) |^ 1)) *' f) | (Segm 1) = (Segm 1) --> (0. INT.Ring)

proof

for x being object st x in dom (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) holds
(((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) . x = ((Segm 1) --> (0. INT.Ring)) . x

proof

let x be object ; :: thesis: ( x in dom (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) implies (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) . x = ((Segm 1) --> (0. INT.Ring)) . x )
assume A3: x in dom (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) ; :: thesis: (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) . x = ((Segm 1) --> (0. INT.Ring)) . x
then (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) . x = ((~ ((tau 0) |^ 1)) *' f) . x by FUNCT_1:49
.= ((~ (tau 0)) *' f) . x by BINOM:8
.= ((tau 0) *' f) . 0 by A3, NAT_1:14, NAT_1:44
.= 0. INT.Ring by Th15 ;
hence (((~ ((tau 0) |^ 1)) *' f) | (Segm 1)) . x = ((Segm 1) --> (0. INT.Ring)) . x by A3, FUNCOP_1:7; :: thesis: verum

end;

hence ((~ ((tau 0) |^ 1)) *' f) | (Segm 1) = (Segm 1) --> (0. INT.Ring) ; :: thesis: verum

end;

A4: S₁[1] by A1, Th15, A2;
A5: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
reconsider fk = (~ ((tau 0) |^ k)) *' f as Element of the carrier of (Polynom-Ring INT.Ring) by POLYNOM3:def 10;
A7: (tau 0) `^ k = (tau 0) |^ k by BINOM:def 2;
A8: ~ ((tau 0) |^ (k + 1)) = (tau 0) `^ (k + 1) by BINOM:def 2
.= (tau 0) *' (~ ((tau 0) |^ k)) by A7, POLYNOM5:19 ;
then A13: (tau 0) *' fk = (~ ((tau 0) |^ (k + 1))) *' f by POLYNOM3:33;
A9: (tau 0) *' fk = (~ ((tau 0) |^ (k + 1))) *' f by A8, POLYNOM3:33;
set ik = i + k;
A10: ((~ ((tau 0) |^ (k + 1))) *' f) . ((i + k) + 1) = fk . (i + k) by A9, Th15
.= f . i by A6 ;
reconsider f1 = (~ ((tau 0) |^ 1)) *' f as Element of the carrier of (Polynom-Ring INT.Ring) by POLYNOM3:def 10;
((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k)) = (Segm (1 + k)) --> (0. INT.Ring)

proof

for x being object st x in dom (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) holds
(((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x

proof

let x be object ; :: thesis: ( x in dom (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) implies (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x )
assume A11: x in dom (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) ; :: thesis: (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x
A12: (Segm k) \/ {k} = Segm (1 + k) by AFINSQ_1:2;

per cases ( x in Segm k or x in {k} ) by A11, XBOOLE_0:def 3, A12;

suppose A14: x in Segm k ; :: thesis: (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x

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

suppose A15: x = 0 ; :: thesis: (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x

A16: ( (tau 0) . 0 = 0. INT.Ring & (tau 0) . 1 = 1. INT.Ring ) by POLYNOM5:38;
(((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((~ ((tau 0) |^ (1 + k))) *' f) . x by A11, FUNCT_1:49
.= ((~ (tau 0)) . 0) * (((~ ((tau 0) |^ k)) *' f) . 0) by Th14, A13, A15
.= ((Segm (k + 1)) --> (0. INT.Ring)) . x by A11, A16, FUNCOP_1:7 ;
hence (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x ; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x

then reconsider x = x as non zero Nat by A11;
reconsider x1 = x - 1 as Element of NAT by INT_1:3;
x - 1 < x by XREAL_1:44;
then A19: x1 < k by XXREAL_0:2, NAT_1:44, A14;
(((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((tau 0) *' fk) . (x1 + 1) by A13, A11, FUNCT_1:49
.= ((~ ((tau 0) |^ k)) *' f) . x1 by Th15
.= ((Segm k) --> (0. INT.Ring)) . x1 by A6, NAT_1:44, A19, FUNCT_1:49
.= 0. INT.Ring by NAT_1:44, A19, FUNCOP_1:7
.= ((Segm (k + 1)) --> (0. INT.Ring)) . x by A11, FUNCOP_1:7 ;
hence (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x ; :: thesis: verum

end;

end;

end;

suppose x in {k} ; :: thesis: (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x

then A21: x = k by TARSKI:def 1;
A22: k - 1 in Segm k by NAT_1:44, XREAL_1:44;
(((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((tau 0) *' fk) . ((k - 1) + 1) by A13, A21, A11, FUNCT_1:49
.= ((~ ((tau 0) |^ k)) *' f) . (k - 1) by Th15
.= ((Segm k) --> (0. INT.Ring)) . (k - 1) by A6, A22, FUNCT_1:49
.= 0. INT.Ring by FUNCOP_1:7, A22
.= ((Segm (k + 1)) --> (0. INT.Ring)) . x by A11, FUNCOP_1:7 ;
hence (((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k))) . x = ((Segm (1 + k)) --> (0. INT.Ring)) . x ; :: thesis: verum

end;

end;

end;

hence ((~ ((tau 0) |^ (1 + k))) *' f) | (Segm (1 + k)) = (Segm (1 + k)) --> (0. INT.Ring) ; :: thesis: verum

end;

hence S₁[k + 1] by A10; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A4, A5);
hence ( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) ) ; :: thesis: verum

end;

hence ( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) ) ; :: thesis: verum