let f be Function; :: thesis: for a, b being object
for A being set holds
( a in A or (f +* (a,b)) | A = f | A )
let a, b be object ; :: thesis: for A being set holds
( a in A or (f +* (a,b)) | A = f | A )
let A be set ; :: thesis: ( a in A or (f +* (a,b)) | A = f | A )

per cases ( a in dom f or not a in dom f ) ;

suppose A1: a in dom f ; :: thesis: ( a in A or (f +* (a,b)) | A = f | A )

assume not a in A ; :: thesis: (f +* (a,b)) | A = f | A
then {a} misses A by ZFMISC_1:50;
then A2: dom (a .--> b) misses A ;
thus (f +* (a,b)) | A = (f +* (a .--> b)) | A by A1, Def2
.= f | A by A2, FUNCT_4:72 ; :: thesis: verum

end;

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

hence ( a in A or (f +* (a,b)) | A = f | A ) by Def2; :: thesis: verum

end;

end;