let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace f,i,p) /. i = p
let f be FinSequence of D; :: thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace f,i,p) /. i = p
let p be Element of D; :: thesis: for i being Nat st 1 <= i & i <= len f holds
(Replace f,i,p) /. i = p
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies (Replace f,i,p) /. i = p )
assume that
A1: 1 <= i and
A2: i <= len f ; :: thesis: (Replace f,i,p) /. i = p
i <= len (Replace f,i,p) by A2, Th7;
then i in dom (Replace f,i,p) by A1, FINSEQ_3:27;
then (Replace f,i,p) /. i = (Replace f,i,p) . i by PARTFUN1:def 8;
hence (Replace f,i,p) /. i = p by A1, A2, Lm2; :: thesis: verum