let R be non degenerated comRing; :: thesis: for D being Derivation of R
for s being FinSequence of the carrier of R st len s = 1 holds
Sum (DProd (D,s)) = D . (Product s)
let D be Derivation of R; :: thesis: for s being FinSequence of the carrier of R st len s = 1 holds
Sum (DProd (D,s)) = D . (Product s)
let s be FinSequence of the carrier of R; :: thesis: ( len s = 1 implies Sum (DProd (D,s)) = D . (Product s) )
assume A1: len s = 1 ; :: thesis: Sum (DProd (D,s)) = D . (Product s)
reconsider Ds1 = D . (s /. 1) as Element of R ;
dom s = Seg 1 by A1, FINSEQ_1:def 3;
then A2: 1 in dom s ;
A3: s = <*(s . 1)*> by A1, FINSEQ_1:40
.= <*(s /. 1)*> by A2, PARTFUN1:def 6 ;
reconsider s1 = s /. 1 as Element of R ;
A4: len (DProd (D,s)) = 1 by A1, Def3;
dom (DProd (D,s)) = Seg 1 by A4, FINSEQ_1:def 3;
then A5: 1 in dom (DProd (D,s)) ;
A6: Replace (s,1,Ds1) = <*Ds1*> by A3, FINSEQ_7:12;
Sum (DProd (D,s)) = (DProd (D,s)) . 1 by A4, RLVECT_1:76
.= Product <*(D . (s /. 1))*> by A6, A5, Def3
.= D . (s /. 1) by GROUP_4:9
.= D . (Product s) by A3, GROUP_4:9 ;
hence Sum (DProd (D,s)) = D . (Product s) ; :: thesis: verum