let x be variable; :: according to ABCMIZ_1:def 58 :: thesis: ( x in dom (f at g) implies ex y being variable st (f at g) . x = y -term C )
assume A0: x in dom (f at g) ; :: thesis: ex y being variable st (f at g) . x = y -term C
then A1: (f at g) . x = ((x -term C) at f) at g by SUBST2;
A2: dom (f at g) = (dom f) \/ (dom g) by SUBST2;

per cases ( x in dom f or x nin dom f ) ;

suppose A3: x in dom f ; :: thesis: ex y being variable st (f at g) . x = y -term C

then consider y being variable such that
A4: f . x = y -term C by IRR;
(x -term C) at f = y -term C by A3, A4, SUBST;
then ( ( y in dom g implies (f at g) . x = g . y ) & ( y nin dom g implies (f at g) . x = y -term C ) ) by A1, SUBST;
hence ex y being variable st (f at g) . x = y -term C by IRR; :: thesis: verum

end;

suppose x nin dom f ; :: thesis: ex y being variable st (f at g) . x = y -term C

then A7: ( (x -term C) at f = x -term C & x in dom g ) by A0, A2, SUBST, XBOOLE_0:def 3;
then (f at g) . x = g . x by A1, SUBST;
hence ex y being variable st (f at g) . x = y -term C by A7, IRR; :: thesis: verum

end;

end;