let IT1, IT2 be Function; :: thesis: ( dom IT1 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

IT1 . x = (f . x) \/ (g . x) ) & dom IT2 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

IT2 . x = (f . x) \/ (g . x) ) implies IT1 = IT2 )

assume that

A4: dom IT1 = (dom f) \/ (dom g) and

A5: for x being object st x in (dom f) \/ (dom g) holds

IT1 . x = (f . x) \/ (g . x) and

A6: dom IT2 = (dom f) \/ (dom g) and

A7: for x being object st x in (dom f) \/ (dom g) holds

IT2 . x = (f . x) \/ (g . x) ; :: thesis: IT1 = IT2

IT1 . x = (f . x) \/ (g . x) ) & dom IT2 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

IT2 . x = (f . x) \/ (g . x) ) implies IT1 = IT2 )

assume that

A4: dom IT1 = (dom f) \/ (dom g) and

A5: for x being object st x in (dom f) \/ (dom g) holds

IT1 . x = (f . x) \/ (g . x) and

A6: dom IT2 = (dom f) \/ (dom g) and

A7: for x being object st x in (dom f) \/ (dom g) holds

IT2 . x = (f . x) \/ (g . x) ; :: thesis: IT1 = IT2

now :: thesis: for x being object st x in dom IT1 holds

IT1 . x = IT2 . x

hence
IT1 = IT2
by A4, A6, FUNCT_1:2; :: thesis: verumIT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )

assume A8: x in dom IT1 ; :: thesis: IT1 . x = IT2 . x

IT1 . x = (f . x) \/ (g . x) by A4, A5, A8;

hence IT1 . x = IT2 . x by A4, A7, A8; :: thesis: verum

end;assume A8: x in dom IT1 ; :: thesis: IT1 . x = IT2 . x

IT1 . x = (f . x) \/ (g . x) by A4, A5, A8;

hence IT1 . x = IT2 . x by A4, A7, A8; :: thesis: verum