let i, n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D 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 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 st i in dom (f | n) holds
(Ins (f,n,p)) . i = f . i
let f be FinSequence of D; :: 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:32
.= (f | n) . i by A1, Lm1
.= f . i by A1, FUNCT_1:47 ; :: thesis: verum