let n be Nat; :: thesis:
let a, b be set ; :: thesis:

A1: now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom (n |-> b) ; :: thesis:
then A2: x in Seg n ;
hence x in dom (n |-> a) ; :: thesis:
( dom (a .--> b) = {a} & (n |-> a) . x = a ) by A2, FUNCOP_1:7;
hence (n |-> a) . x in dom (a .--> b) by TARSKI:def 1; :: thesis:

end;

assume that
A3: x in dom (n |-> a) and
(n |-> a) . x in dom (a .--> b) ; :: thesis:
x in Seg n by A3;
hence x in dom (n |-> b) ; :: thesis:

end;

let x be object ; :: thesis:
A4: a in {a} by TARSKI:def 1;
assume x in dom (n |-> b) ; :: thesis:
then A5: x in Seg n ;
hence (n |-> b) . x = b by FUNCOP_1:7
.= (a .--> b) . a by A4, FUNCOP_1:7
.= (a .--> b) . ((n |-> a) . x) by A5, FUNCOP_1:7 ;
:: thesis:

end;

hence (a .--> b) * (n |-> a) = n |-> b by A1, FUNCT_1:10; :: thesis: