let D be non empty set ; :: thesis: for f being FinSequence of D
for d being Element of D
for i being Element of 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 Element of NAT st i in dom f holds
(f +* i,d) /. i = d
let d be Element of D; :: thesis: for i being Element of NAT st i in dom f holds
(f +* i,d) /. i = d
let i be Element of 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 Th32;
hence (f +* i,d) /. i = (f +* i,d) . i by PARTFUN1:def 8
.= d by A1, Th33 ;
:: thesis: verum