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:32;
A3: dom (g +* a,y) = dom g by FUNCT_7:32;
A4: dom (f +* a,x) = dom f by FUNCT_7:32;

now

thus dom (f +* a,z) = dom f by FUNCT_7:32; :: thesis: ( dom (g +* a,z) = dom f & ( for a being set 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:32; :: thesis: for a being set st a in dom f holds
(f +* a,z) . b₂ = (g +* a,z) . b₂
let a be set ; :: 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:33
.= (g +* a,z) . a by A1, A4, A3, A5, A6, FUNCT_7:33 ;
:: 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:34
.= (g +* a,y) . a by A1, A7, FUNCT_7:34
.= g . a by A7, FUNCT_7:34
.= (g +* a,z) . a by A7, FUNCT_7:34 ;
:: thesis: verum

end;

end;

end;

hence f +* a,z = g +* a,z by FUNCT_1:9; :: thesis: verum