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 A1: x in dom (f at g) ; :: thesis: ex y being variable st (f at g) . x = y -term C
then A2: (f at g) . x = ((x -term C) at f) at g by Def66;
A3: dom (f at g) = (dom f) \/ (dom g) by Def66;
per cases ( x in dom f or x nin dom f ) ;
suppose A4: x in dom f ; :: thesis: ex y being variable st (f at g) . x = y -term C
then consider y being variable such that
A5: f . x = y -term C by Def58;
A6: (x -term C) at f = y -term C by A4, A5, Def60;
then A7: ( y in dom g implies (f at g) . x = g . y ) by A2, Def60;
( y nin dom g implies (f at g) . x = y -term C ) by A2, A6, Def60;
hence ex y being variable st (f at g) . x = y -term C by A7, Def58; :: thesis: verum
end;
suppose A8: x nin dom f ; :: thesis: ex y being variable st (f at g) . x = y -term C
then A9: (x -term C) at f = x -term C by Def60;
A10: x in dom g by A1, A3, A8, XBOOLE_0:def 3;
then (f at g) . x = g . x by A2, A9, Def60;
hence ex y being variable st (f at g) . x = y -term C by A10, Def58; :: thesis: verum
end;
end;