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} by FUNCOP_1:13
.= n \/ {n} by PARTFUN1:def 2
.= succ n by ORDINAL1:def 1
.= n + 1 by NAT_1:38 ;
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) = (n + 1) /\ n by A2, RELAT_1:61
.= (succ n) /\ n by NAT_1:38
.= (n \/ {n}) /\ n by ORDINAL1:def 1
.= n by XBOOLE_1:21 ;

now

let x be set ; :: 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

assume x in dom (n .--> k) ; :: thesis: contradiction
then x in {n} by FUNCOP_1:13;
then x = n by TARSKI:def 1;
hence contradiction by A4; :: 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) by FUNCOP_1:13;
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