let a, x, y, z be set ; :: thesis: for f, g being Function st f +* (a,x) = g +* (a,y) holds
f +* (a,z) = g +* (a,z)
let f, g be Function; :: thesis: ( f +* (a,x) = g +* (a,y) implies f +* (a,z) = g +* (a,z) )
set i = a;
assume A1: f +* (a,x) = g +* (a,y) ; :: thesis: f +* (a,z) = g +* (a,z)
A2: dom (g +* (a,z)) = dom g by FUNCT_7:30;
A3: dom (g +* (a,y)) = dom g by FUNCT_7:30;
A4: dom (f +* (a,x)) = dom f by FUNCT_7:30;

now :: thesis: ( dom (f +* (a,z)) = dom f & dom (g +* (a,z)) = dom f & ( for a being object st a in dom f holds
(f +* (a,z)) . a = (g +* (a,z)) . a ) )

thus dom (f +* (a,z)) = dom f by FUNCT_7:30; :: thesis: ( dom (g +* (a,z)) = dom f & ( for a being object st a in dom f holds
(f +* (a,z)) . b₂ = (g +* (a,z)) . b₂ ) )
thus dom (g +* (a,z)) = dom f by A1, A3, A2, FUNCT_7:30; :: thesis: for a being object st a in dom f holds
(f +* (a,z)) . b₂ = (g +* (a,z)) . b₂
let a be object ; :: thesis: ( a in dom f implies (f +* (a,z)) . b₁ = (g +* (a,z)) . b₁ )
assume A5: a in dom f ; :: thesis: (f +* (a,z)) . b₁ = (g +* (a,z)) . b₁

per cases ( a = a or a <> a ) ;

suppose A6: a = a ; :: thesis: (f +* (a,z)) . b₁ = (g +* (a,z)) . b₁

hence (f +* (a,z)) . a = z by A5, FUNCT_7:31
.= (g +* (a,z)) . a by A1, A4, A3, A5, A6, FUNCT_7:31 ;
:: thesis: verum

end;

suppose A7: a <> a ; :: thesis: (f +* (a,z)) . b₁ = (g +* (a,z)) . b₁

hence (f +* (a,z)) . a = f . a by FUNCT_7:32
.= (g +* (a,y)) . a by A1, A7, FUNCT_7:32
.= g . a by A7, FUNCT_7:32
.= (g +* (a,z)) . a by A7, FUNCT_7:32 ;
:: thesis: verum

end;

end;

end;

hence f +* (a,z) = g +* (a,z) ; :: thesis: verum