let L be domRing; :: thesis: for D being Derivation of L
for f being Element of the carrier of L
for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f)
let D be Derivation of L; :: thesis: for f being Element of the carrier of L
for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f)
for f being Element of the carrier of L
for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f)

proof

let f be Element of the carrier of L; :: thesis: for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f)
let j, n be Nat; :: thesis: (D |^ n) . (j * f) = j * ((D |^ n) . f)
defpred S₁[ Nat] means (D |^ $1) . (j * f) = j * ((D |^ $1) . f);
A1: S₁[ 0 ]

proof

A2: (D |^ 0) . (j * f) = (id L) . (j * f) by VECTSP11:18
.= j * f ;
j * ((D |^ 0) . f) = j * ((id L) . f) by VECTSP11:18
.= j * f ;
hence S₁[ 0 ] by A2; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (D |^ (n + 1)) . (j * f) = D . (j * ((D |^ n) . f)) by RINGDER1:9
.= j * (D . ((D |^ n) . f)) by RINGDER1:6
.= j * ((D |^ (n + 1)) . f) by RINGDER1:9 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence (D |^ n) . (j * f) = j * ((D |^ n) . f) ; :: thesis: verum

end;

hence for f being Element of the carrier of L
for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f) ; :: thesis: verum