let z1, z2 be object ; :: thesis: for f being Function
for x being object holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
let f be Function; :: thesis: for x being object holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
let x be object ; :: thesis: (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)
A1: dom (x .--> z1) = {x}
.= dom (x .--> z2) ;
thus (f +* (x .--> z1)) +* (x .--> z2) = f +* ((x .--> z1) +* (x .--> z2)) by Th14
.= f +* (x .--> z2) by A1, Th19 ; :: thesis: verum