defpred S1[ object , object ] means ( ( \$1 in F1() implies \$2 = F5() . \$1 ) & ( \$1 in F3() \ F1() implies \$2 = F6(\$1) ) );
A4: for x being object st x in F3() holds
ex y being object st
( y in F4() & S1[x,y] )
proof
let x be object ; :: thesis: ( x in F3() implies ex y being object st
( y in F4() & S1[x,y] ) )

assume A5: x in F3() ; :: thesis: ex y being object st
( y in F4() & S1[x,y] )

now :: thesis: ex y being object st
( y in F4() & S1[x,y] )
per cases ( x in F1() or not x in F1() ) ;
suppose A6: x in F1() ; :: thesis: ex y being object st
( y in F4() & S1[x,y] )

then x in dom F5() by ;
then F5() . x in rng F5() by FUNCT_1:def 3;
then A7: F5() . x in F4() by A2;
not x in F3() \ F1() by ;
hence ex y being object st
( y in F4() & S1[x,y] ) by A7; :: thesis: verum
end;
suppose A8: not x in F1() ; :: thesis: ex y being object st
( y in F4() & S1[x,y] )

then x in F3() \ F1() by ;
then F6(x) in F4() by A1;
hence ex y being object st
( y in F4() & S1[x,y] ) by A8; :: thesis: verum
end;
end;
end;
hence ex y being object st
( y in F4() & S1[x,y] ) ; :: thesis: verum
end;
consider h being Function of F3(),F4() such that
A9: for x being object st x in F3() holds
S1[x,h . x] from A10: dom F5() = (dom h) /\ F1()
proof
now :: thesis: dom F5() = (dom h) /\ F1()
per cases ( F2() is empty or not F2() is empty ) ;
suppose F2() is empty ; :: thesis: dom F5() = (dom h) /\ F1()
hence dom F5() = (dom h) /\ F1() by A3; :: thesis: verum
end;
suppose A11: not F2() is empty ; :: thesis: dom F5() = (dom h) /\ F1()
then not F4() is empty by A2;
then A12: dom h = F3() by FUNCT_2:def 1;
dom F5() = F1() by ;
hence dom F5() = (dom h) /\ F1() by ; :: thesis: verum
end;
end;
end;
hence dom F5() = (dom h) /\ F1() ; :: thesis: verum
end;
take h ; :: thesis: ( h | F1() = F5() & ( for x being set st x in F3() \ F1() holds
h . x = F6(x) ) )

for x being object st x in dom F5() holds
h . x = F5() . x
proof
let x be object ; :: thesis: ( x in dom F5() implies h . x = F5() . x )
assume x in dom F5() ; :: thesis: h . x = F5() . x
then x in F1() ;
hence h . x = F5() . x by A2, A9; :: thesis: verum
end;
hence h | F1() = F5() by ; :: thesis: for x being set st x in F3() \ F1() holds
h . x = F6(x)

thus for x being set st x in F3() \ F1() holds
h . x = F6(x) by A9; :: thesis: verum