A2: for e being object st e in F2() holds
ex u being object st
( u in F3() & P1[e,u] )
proof
let e be object ; :: thesis: ( e in F2() implies ex u being object st
( u in F3() & P1[e,u] ) )

assume A3: e in F2() ; :: thesis: ex u being object 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 ; :: thesis: ( u1 in F3() & P1[e,u1] )
thus ( u1 in F3() & P1[e,u1] ) by A4; :: thesis: verum
end;
consider f being Function such that
A5: ( dom f = F2() & rng f c= F3() ) and
A6: for e being object st e in F2() holds
P1[e,f . e] from reconsider f = f as Function of F2(),F3() by ;
take f ; :: thesis: 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(); :: thesis: ( 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() ; :: thesis: 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 ; :: thesis: ( fe in F3() & fe = f . e & P1[e,fe] )
thus ( fe in F3() & fe = f . e & P1[e,fe] ) by A6, A7; :: thesis: 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] ) ; :: thesis: verum