let a, m be Nat; :: thesis: for D being set
for p being FinSequence of D st a in dom (p | m) holds
(p | m) /. a = p /. a
let D be set ; :: thesis: for p being FinSequence of D st a in dom (p | m) holds
(p | m) /. a = p /. a
let p be FinSequence of D; :: thesis: ( a in dom (p | m) implies (p | m) /. a = p /. a )
assume A1: a in dom (p | m) ; :: thesis: (p | m) /. a = p /. a
then a in (dom p) /\ (Seg m) by RELAT_1:61;
then A2: a in dom p by XBOOLE_0:def 4;
thus (p | m) /. a = (p | (Seg m)) . a by A1, PARTFUN1:def 6
.= p . a by A1, FUNCT_1:47
.= p /. a by A2, PARTFUN1:def 6 ; :: thesis: verum