defpred S1[ object , object ] means ( P1[$1,$2] & $2 in F1() );
reconsider X = F1() as set ;
A2:
now for x being object st x in Seg F2() holds
ex y being object st
( y in X & S1[x,y] )let x be
object ;
( x in Seg F2() implies ex y being object st
( y in X & S1[x,y] ) )assume A3:
x in Seg F2()
;
ex y being object st
( y in X & S1[x,y] )then reconsider x9 =
x as
Element of
NAT ;
consider d being
Element of
F1()
such that A4:
P1[
x9,
d]
by A1, A3;
reconsider y =
d as
object ;
take y =
y;
( y in X & S1[x,y] )thus
(
y in X &
S1[
x,
y] )
by A4;
verum end;
consider f being Function such that
A5:
( dom f = Seg F2() & rng f c= X & ( for x being object st x in Seg F2() holds
S1[x,f . x] ) )
from FUNCT_1:sch 6(A2);
reconsider f = f as FinSequence by A5, FINSEQ_1:def 2;
reconsider f = f as FinSequence of F1() by A5, FINSEQ_1:def 4;
take
f
; ( len f = F2() & ( for n being Nat st n in Seg F2() holds
P1[n,f /. n] ) )
F2() in NAT
by ORDINAL1:def 12;
hence
len f = F2()
by A5, FINSEQ_1:def 3; for n being Nat st n in Seg F2() holds
P1[n,f /. n]
let n be Nat; ( n in Seg F2() implies P1[n,f /. n] )
assume A6:
n in Seg F2()
; P1[n,f /. n]
then
P1[n,f . n]
by A5;
hence
P1[n,f /. n]
by A5, A6, PARTFUN1:def 6; verum