defpred S_{1}[ object , object ] means (f . $1) \/ (g . $1) = $2;

set A = (dom f) \/ (dom g);

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

ex y being object st S_{1}[x,y]
;

ex f being Function st

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

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A1);

then consider IT being Function such that

A2: dom IT = (dom f) \/ (dom g) and

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

S_{1}[x,IT . x]
;

take IT ; :: thesis: ( dom IT = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

IT . x = (f . x) \/ (g . x) ) )

thus dom IT = (dom f) \/ (dom g) by A2; :: thesis: for x being object st x in (dom f) \/ (dom g) holds

IT . x = (f . x) \/ (g . x)

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

IT . x = (f . x) \/ (g . x) by A3; :: thesis: verum

set A = (dom f) \/ (dom g);

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

ex y being object st S

ex f being Function st

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

S

then consider IT being Function such that

A2: dom IT = (dom f) \/ (dom g) and

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

S

take IT ; :: thesis: ( dom IT = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

IT . x = (f . x) \/ (g . x) ) )

thus dom IT = (dom f) \/ (dom g) by A2; :: thesis: for x being object st x in (dom f) \/ (dom g) holds

IT . x = (f . x) \/ (g . x)

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

IT . x = (f . x) \/ (g . x) by A3; :: thesis: verum