let IT1, IT2 be Function; :: thesis: ( dom IT1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
IT1 . x = (f . x) \/ (g . x) ) & dom IT2 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
IT2 . x = (f . x) \/ (g . x) ) implies IT1 = IT2 )
assume that
A5: dom IT1 = (dom f) \/ (dom g) and
A6: for x being set st x in (dom f) \/ (dom g) holds
IT1 . x = (f . x) \/ (g . x) and
A7: dom IT2 = (dom f) \/ (dom g) and
A8: for x being set st x in (dom f) \/ (dom g) holds
IT2 . x = (f . x) \/ (g . x) ; :: thesis: IT1 = IT2

now

let x be set ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume A9: x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
IT1 . x = (f . x) \/ (g . x) by A5, A6, A9;
hence IT1 . x = IT2 . x by A5, A8, A9; :: thesis: verum

end;

hence IT1 = IT2 by A5, A7, FUNCT_1:9; :: thesis: verum