let z1, z2 be set ; :: thesis: for f being Function
for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
let f be Function; :: thesis: for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
let x be set ; :: thesis: (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
A1: dom (x .--> z1) = {x} by FUNCOP_1:13
.= dom (x .--> z2) by FUNCOP_1:13 ;
thus (f +* (x .--> z1)) +* (x .--> z2) = f +* ((x .--> z1) +* (x .--> z2)) by Th15
.= f +* (x .--> z2) by A1, Th20 ; :: thesis: verum