defpred S₁[ 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₁[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₁[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₁[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