let f, g be Function; :: thesis: for x, y being object st f c= g & not x in dom f holds
f c= g +* (x,y)
let x, y be object ; :: thesis: ( f c= g & not x in dom f implies f c= g +* (x,y) )
assume A1: f c= g ; :: thesis: ( x in dom f or f c= g +* (x,y) )
assume not x in dom f ; :: thesis: f c= g +* (x,y)
then A2: f c= f +* (x .--> y) by FUNCT_4:107;

per cases ( x in dom g or not x in dom g ) ;

suppose x in dom g ; :: thesis: f c= g +* (x,y)

then g +* (x,y) = g +* (x .--> y) by Def2;
then f +* (x .--> y) c= g +* (x,y) by A1, FUNCT_4:123;
hence f c= g +* (x,y) by A2; :: thesis: verum

end;

suppose not x in dom g ; :: thesis: f c= g +* (x,y)

hence f c= g +* (x,y) by A1, Def2; :: thesis: verum

end;

end;