A2:
for y being object st y in Seg F2() holds
ex x being object st
( x in F1() & P1[y,x] )
proof
let y be
object ;
( y in Seg F2() implies ex x being object st
( x in F1() & P1[y,x] ) )
assume A3:
y in Seg F2()
;
ex x being object st
( x in F1() & P1[y,x] )
then reconsider k =
y as
Element of
NAT ;
consider x being
Element of
F1()
such that A4:
P1[
k,
x]
by A1, A3;
take
x
;
( x in F1() & P1[y,x] )
thus
(
x in F1() &
P1[
y,
x] )
by A4;
verum
end;
consider f being Function such that
A5:
dom f = Seg F2()
and
A6:
rng f c= F1()
and
A7:
for y being object st y in Seg F2() holds
P1[y,f . y]
from FUNCT_1:sch 6(A2);
reconsider f = f as FinSequence by A5, Def2;
reconsider p = f as FinSequence of F1() by A6, Def4;
take
p
; ( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p . k] ) )
thus
( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p . k] ) )
by A5, A7; verum