A2:
for e being set st e in F2() holds
ex u being set st
( u in F3() & P1[e,u] )
proof
let e be
set ;
( e in F2() implies ex u being set st
( u in F3() & P1[e,u] ) )
assume A3:
e in F2()
;
ex u being set st
( u in F3() & P1[e,u] )
then reconsider e1 =
e as
Element of
F2() ;
reconsider e1 =
e1 as
Element of
F1()
by A3;
consider u being
Element of
F1()
such that A4:
(
u in F3() &
P1[
e1,
u] )
by A1, A3;
reconsider u1 =
u as
set ;
take
u1
;
( u1 in F3() & P1[e,u1] )
thus
(
u1 in F3() &
P1[
e,
u1] )
by A4;
verum
end;
consider f being Function such that
A5:
( dom f = F2() & rng f c= F3() )
and
A6:
for e being set st e in F2() holds
P1[e,f . e]
from FUNCT_1:sch 5(A2);
reconsider f = f as Function of F2(),F3() by A5, FUNCT_2:def 1, RELSET_1:4;
take
f
; for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
proof
let e be
Element of
F1();
( e in F2() implies ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] ) )
assume A7:
e in F2()
;
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
then reconsider e1 =
f . e as
Element of
F3()
by FUNCT_2:5;
reconsider fe =
e1 as
Element of
F1() ;
take
fe
;
( fe in F3() & fe = f . e & P1[e,fe] )
thus
(
fe in F3() &
fe = f . e &
P1[
e,
fe] )
by A6, A7;
verum
end;
hence
for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
; verum