let f be Function; :: thesis: for X, y, z being set holds (f +* (X --> y)) +* (X --> z) = f +* (X --> z)
let X, y, z be set ; :: thesis: (f +* (X --> y)) +* (X --> z) = f +* (X --> z)
A1: ( dom (X --> y) = X & dom (X --> z) = X ) by FUNCOP_1:19;
then A2: ( dom (f +* (X --> y)) = (dom f) \/ X & dom (f +* (X --> z)) = (dom f) \/ X ) by FUNCT_4:def 1;
then A3: dom ((f +* (X --> y)) +* (X --> z)) = ((dom f) \/ X) \/ X by A1, FUNCT_4:def 1
.= (dom f) \/ (X \/ X) by XBOOLE_1:4
.= (dom f) \/ X ;

now

let x be set ; :: thesis: ( x in (dom f) \/ X implies ((f +* (X --> y)) +* (X --> z)) . b₁ = (f +* (X --> z)) . b₁ )
assume x in (dom f) \/ X ; :: thesis: ((f +* (X --> y)) +* (X --> z)) . b₁ = (f +* (X --> z)) . b₁

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: ((f +* (X --> y)) +* (X --> z)) . b₁ = (f +* (X --> z)) . b₁

then ( ((f +* (X --> y)) +* (X --> z)) . x = (X --> z) . x & (f +* (X --> z)) . x = (X --> z) . x ) by A1, FUNCT_4:14;
hence ((f +* (X --> y)) +* (X --> z)) . x = (f +* (X --> z)) . x ; :: thesis: verum

end;

suppose A4: not x in X ; :: thesis: ((f +* (X --> y)) +* (X --> z)) . b₁ = (f +* (X --> z)) . b₁

then ((f +* (X --> y)) +* (X --> z)) . x = (f +* (X --> y)) . x by A1, FUNCT_4:12;
then ( ((f +* (X --> y)) +* (X --> z)) . x = f . x & (f +* (X --> z)) . x = f . x ) by A1, A4, FUNCT_4:12;
hence ((f +* (X --> y)) +* (X --> z)) . x = (f +* (X --> z)) . x ; :: thesis: verum

end;

end;

end;

hence (f +* (X --> y)) +* (X --> z) = f +* (X --> z) by A2, A3, FUNCT_1:9; :: thesis: verum