set b1 = b +* (n .--> k);
A1: dom b = n by PARTFUN1:def 2;
A2: dom (b +* (n .--> k)) = (dom b) \/ (dom (n .--> k)) by FUNCT_4:def 1
.= (dom b) \/ {n}
.= (Segm n) \/ {n} by PARTFUN1:def 2
.= Segm (n + 1) by AFINSQ_1:2 ;
then b +* (n .--> k) is ManySortedSet of n + 1 by PARTFUN1:def 2, RELAT_1:def 18;
then reconsider b1 = b +* (n .--> k) as Element of Bags (n + 1) by PRE_POLY:def 12;
take b1 ; :: thesis: ( b1 | n = b & b1 . n = k )
A3: dom (b1 | n) = (Segm (n + 1)) /\ (Segm n) by A2, RELAT_1:61
.= ((Segm n) \/ {n}) /\ (Segm n) by AFINSQ_1:2
.= Segm n by XBOOLE_1:21 ;
now :: thesis: for x being object st x in n holds
(b1 | n) . x = b . x
let x be object ; :: thesis: ( x in n implies (b1 | n) . x = b . x )
assume A4: x in n ; :: thesis: (b1 | n) . x = b . x
then A5: x in (dom b) \/ (dom (n .--> k)) by A1, XBOOLE_0:def 3;
A6: now :: thesis: not x in dom (n .--> k)
assume x in dom (n .--> k) ; :: thesis: contradiction
then x in {n} ;
then A: x = n by TARSKI:def 1;
then reconsider x = x as set ;
not x in x ;
hence contradiction by A4, A; :: thesis: verum
end;
thus (b1 | n) . x = b1 . x by A3, A4, FUNCT_1:47
.= b . x by A5, A6, FUNCT_4:def 1 ; :: thesis: verum
end;
hence b1 | n = b by A3, A1, FUNCT_1:2; :: thesis: b1 . n = k
n in {n} by TARSKI:def 1;
then A7: n in dom (n .--> k) ;
then n in (dom b) \/ (dom (n .--> k)) by XBOOLE_0:def 3;
hence b1 . n = (n .--> k) . n by A7, FUNCT_4:def 1
.= k by FUNCOP_1:72 ;
:: thesis: verum