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 ;
( x in F3() implies ex y being object st
( y in F4() & S1[x,y] ) )
assume A5:
x in F3()
;
ex y being object st
( y in F4() & S1[x,y] )
hence
ex
y being
object st
(
y in F4() &
S1[
x,
y] )
;
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 FUNCT_2:sch 1(A4);
A10:
dom F5() = (dom h) /\ F1()
take
h
; ( 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
hence
h | F1() = F5()
by A10, FUNCT_1:46; 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; verum