defpred S₁[ object , object ] means ( ( $1 in F₁() implies $2 = F₅() . $1 ) & ( $1 in F₃() \ F₁() implies $2 = F₆($1) ) );
A4: for x being object st x in F₃() holds
ex y being object st
( y in F₄() & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in F₃() implies ex y being object st
( y in F₄() & S₁[x,y] ) )
assume A5: x in F₃() ; :: thesis: ex y being object st
( y in F₄() & S₁[x,y] )

now :: thesis: ex y being object st
( y in F₄() & S₁[x,y] )

per cases ( x in F₁() or not x in F₁() ) ;

suppose A6: x in F₁() ; :: thesis: ex y being object st
( y in F₄() & S₁[x,y] )

then x in dom F₅() by A3, FUNCT_2:def 1;
then F₅() . x in rng F₅() by FUNCT_1:def 3;
then A7: F₅() . x in F₄() by A2;
not x in F₃() \ F₁() by A6, XBOOLE_0:def 5;
hence ex y being object st
( y in F₄() & S₁[x,y] ) by A7; :: thesis: verum

end;

suppose A8: not x in F₁() ; :: thesis: ex y being object st
( y in F₄() & S₁[x,y] )

then x in F₃() \ F₁() by A5, XBOOLE_0:def 5;
then F₆(x) in F₄() by A1;
hence ex y being object st
( y in F₄() & S₁[x,y] ) by A8; :: thesis: verum

end;

end;

end;

hence ex y being object st
( y in F₄() & S₁[x,y] ) ; :: thesis: verum

end;

consider h being Function of F₃(),F₄() such that
A9: for x being object st x in F₃() holds
S₁[x,h . x] from FUNCT_2:sch 1(A4);
A10: dom F₅() = (dom h) /\ F₁()

proof

now :: thesis: dom F₅() = (dom h) /\ F₁()

per cases ( F₂() is empty or not F₂() is empty ) ;

suppose F₂() is empty ; :: thesis: dom F₅() = (dom h) /\ F₁()

hence dom F₅() = (dom h) /\ F₁() by A3; :: thesis: verum

end;

suppose A11: not F₂() is empty ; :: thesis: dom F₅() = (dom h) /\ F₁()

then not F₄() is empty by A2;
then A12: dom h = F₃() by FUNCT_2:def 1;
dom F₅() = F₁() by A11, FUNCT_2:def 1;
hence dom F₅() = (dom h) /\ F₁() by A2, A12, XBOOLE_1:28; :: thesis: verum

end;

end;

end;

hence dom F₅() = (dom h) /\ F₁() ; :: thesis: verum

end;

take h ; :: thesis: ( h | F₁() = F₅() & ( for x being set st x in F₃() \ F₁() holds
h . x = F₆(x) ) )
for x being object st x in dom F₅() holds
h . x = F₅() . x

proof

let x be object ; :: thesis: ( x in dom F₅() implies h . x = F₅() . x )
assume x in dom F₅() ; :: thesis: h . x = F₅() . x
then x in F₁() ;
hence h . x = F₅() . x by A2, A9; :: thesis: verum

end;

hence h | F₁() = F₅() by A10, FUNCT_1:46; :: thesis: for x being set st x in F₃() \ F₁() holds
h . x = F₆(x)
thus for x being set st x in F₃() \ F₁() holds
h . x = F₆(x) by A9; :: thesis: verum