let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT
for j, b being Nat st (len f) + 1 <= len a & b = j holds
SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1))
let f be FinSequence of NAT ; :: thesis: for j, b being Nat st (len f) + 1 <= len a & b = j holds
SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1))
let j, b be Nat; :: thesis: ( (len f) + 1 <= len a & b = j implies SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1)) )
assume A10: (len f) + 1 <= len a ; :: thesis: ( not b = j or SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1)) )
assume A15: b = j ; :: thesis: SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1))
len (f ^ <*b*>) = (len f) + 1 by FINSEQ_2:16;
then A20: dom (f ^ <*b*>) c= dom a by A10, FINSEQ_3:30;
(f ^ <*b*>) " {j} c= dom (f ^ <*b*>) by RELAT_1:132;
then A30: (f ^ <*b*>) " {j} c= dom a by A20;
A40: (f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)} by A15, NF100;
A59: for m being Nat st m in f " {j} holds
m < (len f) + 1

proof

let m be Nat; :: thesis: ( m in f " {j} implies m < (len f) + 1 )
assume B00: m in f " {j} ; :: thesis: m < (len f) + 1
f " {j} c= dom f by RELAT_1:132;
then m <= len f by B00, FINSEQ_3:25;
hence m < (len f) + 1 by NAT_1:13; :: thesis: verum

end;

Seq (a,((f ^ <*b*>) " {j})) = Seq (a | ((f ^ <*b*>) " {j}))
.= (Seq (a | (f " {j}))) ^ <*(a . ((len f) + 1))*> by A30, A40, A59, NF120
.= (Seq (a,(f " {j}))) ^ <*(a . ((len f) + 1))*> ;
hence SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1)) by RVSUM_1:74; :: thesis: verum