let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let p be Element of D; :: thesis: for f being FinSequence st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let f be FinSequence; :: thesis: ( p in rng f implies (f -| p) ^ <*p*> = f | (p .. f) )
assume A1: p in rng f ; :: thesis: (f -| p) ^ <*p*> = f | (p .. f)
then consider n being Nat such that
A2: n = (p .. f) - 1 and
A3: f -| p = f | (Seg n) by FINSEQ_4:def 5;
( n + 1 in dom f & f . (n + 1) = p ) by A1, A2, FINSEQ_4:19, FINSEQ_4:20;
hence (f -| p) ^ <*p*> = f | (p .. f) by A2, A3, Th10; :: thesis: verum