set D = Der1 INT.Ring;
let i be Nat; :: thesis: (Der1 INT.Ring) . (tau i) = 1. (Polynom-Ring INT.Ring)
len (tau i) = 2 by POLYNOM5:40;
then A2: len ((Der1 INT.Ring) . (tau i)) = 2 - 1 by RING_3:76, E_TRANS1:17
.= 1 ;
((Der1 INT.Ring) . (tau i)) . 0 = (0 + 1) * ((tau i) . (0 + 1)) by RINGDER1:def 8
.= <%(In ((- i),INT.Ring)),(1. INT.Ring)%> . 1 by BINOM:13
.= 1. INT.Ring by POLYNOM5:38 ;
then (Der1 INT.Ring) . (tau i) = <%(1. INT.Ring)%> by A2, UPROOTS:19
.= 1_. INT.Ring by UPROOTS:31 ;
hence (Der1 INT.Ring) . (tau i) = 1. (Polynom-Ring INT.Ring) by POLYNOM3:def 10; :: thesis: verum