defpred S₁[ object , object ] means for y, z being object st $2 `1 = y & $2 `2 = z holds
P₁[$1,y,z];
A2: for x being object st x in F₁() holds
ex p being object st
( p in [:F₂(),F₃():] & S₁[x,p] )

proof

let x be object ; :: thesis: ( x in F₁() implies ex p being object st
( p in [:F₂(),F₃():] & S₁[x,p] ) )
assume x in F₁() ; :: thesis: ex p being object st
( p in [:F₂(),F₃():] & S₁[x,p] )
then consider y, z being object such that
A3: ( y in F₂() & z in F₃() ) and
A4: P₁[x,y,z] by A1;
reconsider p = [y,z] as set ;
take p ; :: thesis: ( p in [:F₂(),F₃():] & S₁[x,p] )
thus p in [:F₂(),F₃():] by A3, ZFMISC_1:87; :: thesis: S₁[x,p]
thus for y, z being object st p `1 = y & p `2 = z holds
P₁[x,y,z] by A4; :: thesis: verum

end;

consider h being Function such that
( dom h = F₁() & rng h c= [:F₂(),F₃():] ) and
A5: for x being object st x in F₁() holds
S₁[x,h . x] from FUNCT_1:sch 6(A2);
deffunc H₁( object ) -> object = (h . $1) `2 ;
deffunc H<sub>2</sub>( object ) -> object = (h . $1) `1 ;
consider f being Function such that
A6: dom f = F₁() and
A7: for x being object st x in F₁() holds
f . x = H₂(x) from FUNCT_1:sch 3();
consider g being Function such that
A8: dom g = F₁() and
A9: for x being object st x in F₁() holds
g . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis: ex g being Function st
( dom f = F₁() & dom g = F₁() & ( for x being object st x in F₁() holds
P₁[x,f . x,g . x] ) )
take g ; :: thesis: ( dom f = F₁() & dom g = F₁() & ( for x being object st x in F₁() holds
P₁[x,f . x,g . x] ) )
thus ( dom f = F₁() & dom g = F₁() ) by A6, A8; :: thesis: for x being object st x in F₁() holds
P₁[x,f . x,g . x]
thus for x being object st x in F₁() holds
P₁[x,f . x,g . x] :: thesis: verum

proof

let x be object ; :: thesis: ( x in F₁() implies P₁[x,f . x,g . x] )
assume A10: x in F₁() ; :: thesis: P₁[x,f . x,g . x]
then ( f . x = (h . x) `1 & g . x = (h . x) `2 ) by A7, A9;
hence P₁[x,f . x,g . x] by A5, A10; :: thesis: verum

end;