let p be prime odd Nat; :: thesis: for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for k being Nat st k in Seg m holds
( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )
let m be positive Nat; :: thesis: for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for k being Nat st k in Seg m holds
( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )
let g be non zero Polynomial of INT.Ring; :: thesis: for z0 being non zero Element of F_Real
for k being Nat st k in Seg m holds
( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )
let z0 be non zero Element of F_Real; :: thesis: for k being Nat st k in Seg m holds
( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )
let k be Nat; :: thesis: ( k in Seg m implies ( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) ) )
assume A1: k in Seg m ; :: thesis: ( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )
then A2: ( 1 <= k & k <= m ) by FINSEQ_1:1;
A3: len (delta_1 (m,p,g)) = m by Def5;
len (delta_2 (m,p,g,z0)) = m by Def6;
then A5: ( k in dom (delta_1 (m,p,g)) & k in dom (delta_2 (m,p,g,z0)) ) by A1, A3, FINSEQ_1:def 3;
A6: dom (delta (m,p,g,z0)) = dom (delta_1 (m,p,g)) by BINOM:def 1
.= Seg m by A3, FINSEQ_1:def 3 ;
Seg (len (delta (m,p,g,z0))) = dom (delta (m,p,g,z0)) by FINSEQ_1:def 3
.= dom (delta_1 (m,p,g)) by BINOM:def 1
.= Seg (len (delta_1 (m,p,g))) by FINSEQ_1:def 3 ;
then A7: len (delta (m,p,g,z0)) = len (delta_1 (m,p,g)) by FINSEQ_1:6
.= m by Def5 ;
A8: (delta_2 (m,p,g,z0)) . k = (delta_2 (m,p,g,z0)) /. k by A5, PARTFUN1:def 6;
(delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) + (delta_2 (m,p,g,z0))) /. k by A1, A6, PARTFUN1:def 6
.= ((delta_1 (m,p,g)) /. k) + ((delta_2 (m,p,g,z0)) /. k) by A2, A7, BINOM:def 1
.= ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) by A5, PARTFUN1:def 6, A8 ;
hence ( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) ) by A1, A6, PARTFUN1:def 6; :: thesis: verum