let D be non empty set ; :: thesis: for f being FinSequence of D
for d being Element of D
for i, j being 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 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 Nat st i <> j & j in dom f holds
(f +* (i,d)) /. j = f /. j
let i, j be 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, Th29;
hence (f +* (i,d)) /. j = (f +* (i,d)) . j by PARTFUN1:def 6
.= f . j by A1, Th31
.= f /. j by A2, PARTFUN1:def 6 ;
:: thesis: verum