let k be Nat; :: thesis: for j being Nat st j > k holds
for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring)
set L = Polynom-Ring INT.Ring;
set D = Der1 INT.Ring;
let j be Nat; :: thesis: ( j > k implies for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring) )
assume A1: j > k ; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring)
for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring)

proof

let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) implies ((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring) )
assume A2: ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) ; :: thesis: ((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring)
A3: j - k > k - k by A1, XREAL_1:8;
then j - k in NAT by INT_1:3;
then reconsider l = j - k as Nat ;
reconsider l1 = l - 1 as Nat by A3, NAT_1:14;
l + k = j ;
then ((Der1 INT.Ring) |^ j) . (f |^ k) = (((Der1 INT.Ring) |^ l) * ((Der1 INT.Ring) |^ k)) . (f |^ k) by VECTSP11:20
.= ((Der1 INT.Ring) |^ l) . (((Der1 INT.Ring) |^ k) . (f |^ k)) by FUNCT_2:15
.= ((Der1 INT.Ring) |^ (l1 + 1)) . ((k !) * (1. (Polynom-Ring INT.Ring))) by A2, Th20
.= (((Der1 INT.Ring) |^ l1) * ((Der1 INT.Ring) |^ 1)) . ((k !) * (1. (Polynom-Ring INT.Ring))) by VECTSP11:20
.= ((Der1 INT.Ring) |^ l1) . (((Der1 INT.Ring) |^ 1) . ((k !) * (1. (Polynom-Ring INT.Ring)))) by FUNCT_2:15
.= ((Der1 INT.Ring) |^ l1) . ((Der1 INT.Ring) . ((k !) * (1. (Polynom-Ring INT.Ring)))) by Lm12
.= ((Der1 INT.Ring) |^ l1) . ((k !) * ((Der1 INT.Ring) . (1. (Polynom-Ring INT.Ring)))) by RINGDER1:6
.= ((Der1 INT.Ring) |^ l1) . ((k !) * (0. (Polynom-Ring INT.Ring))) by RINGDER1:5
.= ((Der1 INT.Ring) |^ l1) . (0 * (1. (Polynom-Ring INT.Ring))) by BINOM:12
.= 0 * (((Der1 INT.Ring) |^ l1) . (1. (Polynom-Ring INT.Ring))) by Th18
.= 0. (Polynom-Ring INT.Ring) by BINOM:12 ;
hence ((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring) ; :: thesis: verum

end;

hence for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring) ; :: thesis: verum