let D be non empty set ; :: thesis: for f being FinSequence of D
for d being Element of D
for i, j being Element of NAT st i <> j & j in dom f holds
(f +* i,d) /. j = f /. j
let f be FinSequence of D; :: thesis: for d being Element of D
for i, j being Element of NAT st i <> j & j in dom f holds
(f +* i,d) /. j = f /. j
let d be Element of D; :: thesis: for i, j being Element of NAT st i <> j & j in dom f holds
(f +* i,d) /. j = f /. j
let i, j be Element of NAT ; :: thesis: ( i <> j & j in dom f implies (f +* i,d) /. j = f /. j )
assume that
A1: i <> j and
A2: j in dom f ; :: thesis: (f +* i,d) /. j = f /. j
j in dom (f +* i,d) by A2, Th32;
hence (f +* i,d) /. j = (f +* i,d) . j by PARTFUN1:def 8
.= f . j by A1, Th34
.= f /. j by A2, PARTFUN1:def 8 ;
:: thesis: verum