set DR = Der1 INT.Ring;
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( len f > 0 implies ('G' f) . (len f) is constant Element of the carrier of (Polynom-Ring INT.Ring) )
assume A1: len f > 0 ; :: thesis: ('G' f) . (len f) is constant Element of the carrier of (Polynom-Ring INT.Ring)
len ('G' f) = len f by Def9;
then A2: dom ('G' f) = Seg (len f) by FINSEQ_1:def 3;
reconsider j1 = (len f) -' 1 as Nat ;
A3: (len f) -' 1 = (len f) - 1 by A1, NAT_1:14, XREAL_1:233;
then len (((Der1 INT.Ring) |^ j1) . f) = (len f) - ((len f) -' 1) by RING_3:76, XREAL_1:44, Th24
.= 1 by A3 ;
then ((Der1 INT.Ring) |^ j1) . f is constant ;
hence ('G' f) . (len f) is constant Element of the carrier of (Polynom-Ring INT.Ring) by A1, A2, FINSEQ_1:3, Def9; :: thesis: verum