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

proof

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

proof

let x1, x2 be set ; :: thesis: ( p `1 = x1 & p `2 = x2 implies P₁[x,x1,x2] )
assume that
A5: p `1 = x1 and
A6: p `2 = x2 ; :: thesis: P₁[x,x1,x2]
x1 = y by A5, MCART_1:7;
hence P₁[x,x1,x2] by A4, A6, MCART_1:7; :: thesis: verum

end;

end;

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

proof

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

end;