let n be Nat; :: thesis: for a, b being set holds (a .--> b) * (n |-> a) = n |-> b
let a, b be set ; :: thesis: (a .--> b) * (n |-> a) = n |-> b

A1: now :: thesis: for x being object holds
( ( x in dom (n |-> b) implies ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) ) ) & ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) implies x in dom (n |-> b) ) )

let x be object ; :: thesis: ( ( x in dom (n |-> b) implies ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) ) ) & ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) implies x in dom (n |-> b) ) )

hereby :: thesis: ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) implies x in dom (n |-> b) )

assume x in dom (n |-> b) ; :: thesis: ( x in dom (n |-> a) & (n |-> a) . x in dom (a .--> b) )
then A2: x in Seg n ;
hence x in dom (n |-> a) ; :: thesis: (n |-> a) . x in dom (a .--> b)
( 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: verum

end;

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

end;

now :: thesis: for x being object st x in dom (n |-> b) holds
(n |-> b) . x = (a .--> b) . ((n |-> a) . x)

let x be object ; :: thesis: ( x in dom (n |-> b) implies (n |-> b) . x = (a .--> b) . ((n |-> a) . x) )
A4: a in {a} by TARSKI:def 1;
assume x in dom (n |-> b) ; :: thesis: (n |-> b) . x = (a .--> b) . ((n |-> a) . x)
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: verum

end;

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