let D be non empty set ; :: thesis: for p being Element of D
for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let p be Element of D; :: thesis: for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let D be set ; :: thesis: for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)
let f be FinSequence of D; :: 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 6;
( n + 1 in dom f & f . (n + 1) = p ) by A1, A2, FINSEQ_4:29, FINSEQ_4:30;
hence (f -| p) ^ <*p*> = f | (p .. f) by A2, A3, Th11; :: thesis: verum