let h1, h2 be valuation of C; :: thesis: ( dom h1 = (dom f) \/ (dom g) & ( for x being variable st x in dom h1 holds
h1 . x = ((x -term C) at f) at g ) & dom h2 = (dom f) \/ (dom g) & ( for x being variable st x in dom h2 holds
h2 . x = ((x -term C) at f) at g ) implies h1 = h2 )
assume that
A5: dom h1 = (dom f) \/ (dom g) and
A6: for x being variable st x in dom h1 holds
h1 . x = ((x -term C) at f) at g and
A7: dom h2 = (dom f) \/ (dom g) and
A8: for x being variable st x in dom h2 holds
h2 . x = ((x -term C) at f) at g ; :: thesis: h1 = h2

now :: thesis: for x being variable st x in dom h1 holds
h1 . x = h2 . x

let x be variable; :: thesis: ( x in dom h1 implies h1 . x = h2 . x )
assume A9: x in dom h1 ; :: thesis: h1 . x = h2 . x
then h1 . x = ((x -term C) at f) at g by A6;
hence h1 . x = h2 . x by A5, A7, A8, A9; :: thesis: verum

end;

hence h1 = h2 by A5, A7; :: thesis: verum