let a be non empty FinSequence of REAL ; 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 ; 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; ( (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
; ( not b = j or SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1)) )
assume A15:
b = j
; 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
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; verum