let R be non degenerated comRing; :: thesis: for D being Derivation of R
for t being FinSequence of the carrier of R st len t >= 1 holds
Sum (DProd (D,t)) = D . (Product t)
let D be Derivation of R; :: thesis: for t being FinSequence of the carrier of R st len t >= 1 holds
Sum (DProd (D,t)) = D . (Product t)
let t be FinSequence of the carrier of R; :: thesis: ( len t >= 1 implies Sum (DProd (D,t)) = D . (Product t) )
assume A1: len t >= 1 ; :: thesis: Sum (DProd (D,t)) = D . (Product t)
defpred S₁[ non zero Nat] means for s being FinSequence of the carrier of R st len s = $1 holds
Sum (DProd (D,s)) = D . (Product s);
A2: S₁[1] by Th13;
A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
for s being FinSequence of the carrier of R st len s = k + 1 holds
Sum (DProd (D,s)) = D . (Product s)

proof

let s be FinSequence of the carrier of R; :: thesis: ( len s = k + 1 implies Sum (DProd (D,s)) = D . (Product s) )
assume A5: len s = k + 1 ; :: thesis: Sum (DProd (D,s)) = D . (Product s)
then A6: dom s = Seg (k + 1) by FINSEQ_1:def 3;
A7: dom (DProd (D,s)) = Seg (len (DProd (D,s))) by FINSEQ_1:def 3
.= Seg (k + 1) by A5, Def3 ;
A8: ( 1 <= k + 1 & k + 1 <= k + 1 ) by NAT_1:11;
then A9: k + 1 in dom s by A6;
A10: k + 1 in dom (DProd (D,s)) by A7, A8;
reconsider sk1 = s /. (k + 1) as Element of R ;
A11: k < len s by A5, XREAL_1:29;
then A12: len (s | k) = k by FINSEQ_1:59;
A13: (s | k) ^ <*(s /. (k + 1))*> = (s | k) ^ <*(s . (k + 1))*> by A9, PARTFUN1:def 6
.= s | (k + 1) by A5, XREAL_1:29, FINSEQ_5:83 ;
A14: (Product (s | k)) * (D . (s /. (k + 1))) = (DProd (D,s)) /. (k + 1)

proof

A15: Replace (s,(k + 1),(D . (s /. (k + 1)))) = ((s | ((k + 1) -' 1)) ^ <*(D . (s /. (k + 1)))*>) ^ (s /^ (k + 1)) by A5, A8, FINSEQ_7:def 1
.= ((s | k) ^ <*(D . (s /. (k + 1)))*>) ^ (s /^ (k + 1)) by NAT_D:34
.= ((s | k) ^ <*(D . (s /. (k + 1)))*>) ^ {} by A5, RFINSEQ:27
.= (s | k) ^ <*(D . (s /. (k + 1)))*> by FINSEQ_1:34 ;
(Product (s | k)) * (D . (s /. (k + 1))) = Product (Replace (s,(k + 1),(D . (s /. (k + 1))))) by A15, GROUP_4:6
.= (DProd (D,s)) . (k + 1) by A10, Def3
.= (DProd (D,s)) /. (k + 1) by A10, PARTFUN1:def 6 ;
hence (Product (s | k)) * (D . (s /. (k + 1))) = (DProd (D,s)) /. (k + 1) ; :: thesis: verum

end;

A16: dom (DProd (D,(s | k))) = Seg (len (DProd (D,(s | k)))) by FINSEQ_1:def 3
.= Seg (len (s | k)) by Def3
.= Seg k by FINSEQ_1:59, A11 ;
reconsider sk1 = s /. (k + 1) as Element of R ;
A17: for i being Nat st i in dom (DProd (D,(s | k))) holds
(sk1 * (DProd (D,(s | k)))) /. i = (DProd (D,s)) . i

proof

let i be Nat; :: thesis: ( i in dom (DProd (D,(s | k))) implies (sk1 * (DProd (D,(s | k)))) /. i = (DProd (D,s)) . i )
assume A18: i in dom (DProd (D,(s | k))) ; :: thesis: (sk1 * (DProd (D,(s | k)))) /. i = (DProd (D,s)) . i
then A19: (DProd (D,(s | k))) /. i = (DProd (D,(s | k))) . i by PARTFUN1:def 6
.= Product (Replace ((s | k),i,(D . ((s | k) /. i)))) by A18, Def3 ;
A20: ( 1 <= i & i <= k ) by FINSEQ_1:1, A18, A16;
then A21: ( 1 <= i & i <= len (s | k) ) by FINSEQ_1:59, A11;
( 1 <= k & k <= k + 1 ) by A20, XXREAL_0:2, NAT_1:11;
then A23: k in dom s by A6;
reconsider i1 = i -' 1 as Nat ;
i - 1 <= k - 0 by A20, XREAL_1:13;
then i -' 1 <= k by A20, XREAL_1:233;
then A26: Seg (i -' 1) c= Seg k by FINSEQ_1:5;
A27: ((s | k) /^ i) ^ <*(s /. (k + 1))*> = ((s | k) ^ <*(s /. (k + 1))*>) /^ i by A21, GENEALG1:1
.= ((s | k) ^ <*(s . (k + 1))*>) /^ i by A9, PARTFUN1:def 6
.= s /^ i by A5, RFINSEQ:7 ;
A28: i <= len s by A5, A20, NAT_1:13;
i <= k + 1 by A20, NAT_1:13;
then A30: i in dom (DProd (D,s)) by A7, A20;
A31: (Replace ((s | k),i,(D . ((s | k) /. i)))) ^ <*(s /. (k + 1))*> = ((((s | k) | (i -' 1)) ^ <*(D . ((s | k) /. i))*>) ^ ((s | k) /^ i)) ^ <*(s /. (k + 1))*> by A21, FINSEQ_7:def 1
.= (((s | (i -' 1)) ^ <*(D . ((s | k) /. i))*>) ^ ((s | k) /^ i)) ^ <*(s /. (k + 1))*> by A26, FUNCT_1:51
.= ((s | (i -' 1)) ^ <*(D . ((s | k) /. i))*>) ^ (s /^ i) by A27, FINSEQ_1:32
.= Replace (s,i,(D . ((s | k) /. i))) by A20, A28, FINSEQ_7:def 1
.= Replace (s,i,(D . (s /. i))) by A23, A18, A16, FINSEQ_4:71 ;
((s /. (k + 1)) * (DProd (D,(s | k)))) /. i = (Product (Replace ((s | k),i,(D . ((s | k) /. i))))) * (s /. (k + 1)) by A19, A18, POLYNOM1:def 1
.= Product (Replace (s,i,(D . (s /. i)))) by A31, GROUP_4:6
.= (DProd (D,s)) . i by Def3, A30 ;
hence (sk1 * (DProd (D,(s | k)))) /. i = (DProd (D,s)) . i ; :: thesis: verum

end;

A32: (Product (s | k)) * (s /. (k + 1)) = Product (s | (k + 1)) by A13, GROUP_4:6
.= Product s by A5, FINSEQ_1:58 ;
A33: ((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*> = DProd (D,s)

proof

set F = (s /. (k + 1)) * (DProd (D,(s | k)));
A34: len ((s /. (k + 1)) * (DProd (D,(s | k)))) = len (DProd (D,(s | k))) by MATRIXR1:16
.= len (s | k) by Def3
.= k by FINSEQ_1:59, A11 ;
then A35: dom ((s /. (k + 1)) * (DProd (D,(s | k)))) = Seg k by FINSEQ_1:def 3;
A36: len (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) = k + 1 by A34, FINSEQ_2:16;
for i being Nat st 1 <= i & i <= len (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) holds
(((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) implies (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i )
assume ( 1 <= i & i <= len (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) ) ; :: thesis: (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i
then i in Seg (k + 1) by A36;

per cases then ( i in Seg k or i = k + 1 ) by FINSEQ_2:7;

suppose A39: i in Seg k ; :: thesis: (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i

then (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = ((s /. (k + 1)) * (DProd (D,(s | k)))) . i by A35, FINSEQ_1:def 7
.= ((s /. (k + 1)) * (DProd (D,(s | k)))) /. i by PARTFUN1:def 6, A39, A35
.= (DProd (D,s)) . i by A17, A16, A39 ;
hence (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i ; :: thesis: verum

end;

suppose A40: i = k + 1 ; :: thesis: (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i

then (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) /. (k + 1) by A34, FINSEQ_1:42
.= (DProd (D,s)) . (k + 1) by PARTFUN1:def 6, A7, FINSEQ_1:4 ;
hence (((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*>) . i = (DProd (D,s)) . i by A40; :: thesis: verum

end;

end;

end;

hence ((s /. (k + 1)) * (DProd (D,(s | k)))) ^ <*((DProd (D,s)) /. (k + 1))*> = DProd (D,s) by A36, A5, Def3; :: thesis: verum

end;

D . (Product s) = ((s /. (k + 1)) * (D . (Product (s | k)))) + ((Product (s | k)) * (D . (s /. (k + 1)))) by Def1, A32
.= ((s /. (k + 1)) * (Sum (DProd (D,(s | k))))) + ((Product (s | k)) * (D . (s /. (k + 1)))) by A4, A12
.= (Sum ((s /. (k + 1)) * (DProd (D,(s | k))))) + ((DProd (D,s)) /. (k + 1)) by A14, POLYNOM1:12
.= Sum (DProd (D,s)) by A33, FVSUM_1:71 ;
hence Sum (DProd (D,s)) = D . (Product s) ; :: thesis: verum

end;

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

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A2, A3);
hence Sum (DProd (D,t)) = D . (Product t) by A1; :: thesis: verum