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 --> z) = X by FUNCOP_1:19;
A2: dom (X --> y) = X by FUNCOP_1:19;
then dom (f +* (X --> y)) = (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 ;

A4: 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 A5: x in X ; :: thesis: ((f +* (X --> y)) +* (X --> z)) . b₁ = (f +* (X --> z)) . b₁

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

end;

suppose A6: 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 by A2, A6, FUNCT_4:12;
hence ((f +* (X --> y)) +* (X --> z)) . x = (f +* (X --> z)) . x by A1, A6, FUNCT_4:12; :: thesis: verum

end;

end;

end;

dom (f +* (X --> z)) = (dom f) \/ X by A1, FUNCT_4:def 1;
hence (f +* (X --> y)) +* (X --> z) = f +* (X --> z) by A3, A4, FUNCT_1:9; :: thesis: verum