let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins f,n,p) /. i = f /. i
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins f,n,p) /. i = f /. i
let p be Element of D; :: thesis: for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins f,n,p) /. i = f /. i
let f be FinSequence of D; :: thesis: for i being Nat st i in dom (f | n) holds
(Ins f,n,p) /. i = f /. i
let i be Nat; :: thesis: ( i in dom (f | n) implies (Ins f,n,p) /. i = f /. i )
assume A1: i in dom (f | n) ; :: thesis: (Ins f,n,p) /. i = f /. i
thus (Ins f,n,p) /. i = ((f | n) ^ (<*p*> ^ (f /^ n))) /. i by FINSEQ_1:45
.= (f | n) /. i by A1, Lm1
.= f /. i by A1, FINSEQ_4:85 ; :: thesis: verum