let f, g be Function; :: thesis: for a, b being object
for A being set st f | A = g | A holds
(f +* (a,b)) | A = (g +* (a,b)) | A
let a, b be object ; :: thesis: for A being set st f | A = g | A holds
(f +* (a,b)) | A = (g +* (a,b)) | A
let 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 :: thesis: a in dom f

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:61;
then not a in (dom g) /\ A by RELAT_1:61;
hence contradiction by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

hence (f +* (a,b)) | A = (f +* (a .--> b)) | A by Def2
.= (g | A) +* ((a .--> b) | A) by A1, FUNCT_4:71
.= (g +* (a .--> b)) | A by FUNCT_4:71
.= (g +* (a,b)) | A by A3, Def2 ;
:: 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 :: thesis: not a in dom f

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:61;
then a in (dom g) /\ A by RELAT_1:61;
hence contradiction by A5, XBOOLE_0:def 4; :: thesis: verum

end;

hence (f +* (a,b)) | A = g | A by A1, Def2
.= (g +* (a,b)) | A by A5, Def2 ;
:: 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 Th91
.= (g +* (a,b)) | A by A1, A6, Th91 ;
:: thesis: verum

end;

end;