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 ;

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

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

hence
b1 | n = b
by A3, A1, FUNCT_1:2; :: thesis: b1 . n = k(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;

.= b . x by A5, A6, FUNCT_4:def 1 ; :: thesis: verum

end;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)

thus (b1 | n) . x =
b1 . x
by A3, A4, FUNCT_1:47
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;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

.= b . x by A5, A6, FUNCT_4:def 1 ; :: thesis: verum

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