let D be non empty set ; :: thesis: for f being FinSequence of D
for d being Element of D
for i being Nat st i in dom f holds
(f +* (i,d)) /. i = d
let f be FinSequence of D; :: thesis: for d being Element of D
for i being Nat st i in dom f holds
(f +* (i,d)) /. i = d
let d be Element of D; :: thesis: for i being Nat st i in dom f holds
(f +* (i,d)) /. i = d
let i be Nat; :: thesis: ( i in dom f implies (f +* (i,d)) /. i = d )
assume A1: i in dom f ; :: thesis: (f +* (i,d)) /. i = d
then i in dom (f +* (i,d)) by Th29;
hence (f +* (i,d)) /. i = (f +* (i,d)) . i by PARTFUN1:def 6
.= d by A1, Th30 ;
:: thesis: verum