let f, g be Function; :: thesis: for a, b, A being set st f | A = g | A holds
(f +* a,b) | A = (g +* a,b) | A
let a, b, A be set ; :: thesis: ( f | A = g | A implies (f +* a,b) | A = (g +* a,b) | A )
assume A1: f | A = g | A ; :: thesis: (f +* a,b) | A = (g +* a,b) | A

per cases ( ( a in A & a in dom g ) or ( a in A & not a in dom g ) or not a in A ) ;

suppose that A2: a in A and
A3: a in dom g ; :: thesis: (f +* a,b) | A = (g +* a,b) | A

now

assume not a in dom f ; :: thesis: contradiction
then not a in (dom f) /\ A by XBOOLE_0:def 4;
then not a in dom (g | A) by A1, RELAT_1:90;
then not a in (dom g) /\ A by RELAT_1:90;
hence contradiction by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

hence (f +* a,b) | A = (f +* (a .--> b)) | A by Def3
.= (g | A) +* ((a .--> b) | A) by A1, FUNCT_4:75
.= (g +* (a .--> b)) | A by FUNCT_4:75
.= (g +* a,b) | A by A3, Def3 ;
:: thesis: verum

end;

suppose that A4: a in A and
A5: not a in dom g ; :: thesis: (f +* a,b) | A = (g +* a,b) | A

now

assume a in dom f ; :: thesis: contradiction
then a in (dom f) /\ A by A4, XBOOLE_0:def 4;
then a in dom (g | A) by A1, RELAT_1:90;
then a in (dom g) /\ A by RELAT_1:90;
hence contradiction by A5, XBOOLE_0:def 4; :: thesis: verum

end;

hence (f +* a,b) | A = g | A by A1, Def3
.= (g +* a,b) | A by A5, Def3 ;
:: thesis: verum

end;

suppose A6: not a in A ; :: thesis: (f +* a,b) | A = (g +* a,b) | A

hence (f +* a,b) | A = f | A by Th94
.= (g +* a,b) | A by A1, A6, Th94 ;
:: thesis: verum

end;

end;