reconsider n = n as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat, object ] means for s being natural Number st s = $1 - 1 holds
$2 = n choose s;
A1: for l being Nat st l in Seg (n + 1) holds
ex x being object st S₁[l,x]

proof

let l be Nat; :: thesis: ( l in Seg (n + 1) implies ex x being object st S₁[l,x] )
assume l in Seg (n + 1) ; :: thesis: ex x being object st S₁[l,x]
then l >= 1 by FINSEQ_1:1;
then reconsider k = l - 1 as Element of NAT by INT_1:5;
set x = n choose k;
take n choose k ; :: thesis: S₁[l,n choose k]
thus S₁[l,n choose k] ; :: thesis: verum

end;

consider F being FinSequence such that
A2: ( dom F = Seg (n + 1) & ( for l being Nat st l in Seg (n + 1) holds
S₁[l,F . l] ) ) from FINSEQ_1:sch 1(A1);
rng F c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in REAL )
assume x in rng F ; :: thesis: x in REAL
then consider y being object such that
A3: y in dom F and
A4: x = F . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A3;
y >= 1 by A2, A3, FINSEQ_1:1;
then reconsider m1 = y - 1 as Element of NAT by INT_1:5;
F . y = n choose m1 by A2, A3;
then reconsider x = x as Real by A4;
x in REAL by XREAL_0:def 1;
hence x in REAL ; :: thesis: verum

end;

then reconsider F = F as FinSequence of REAL by FINSEQ_1:def 4;
take F ; :: thesis: ( len F = n + 1 & ( for i, k being Nat st i in dom F & k = i - 1 holds
F . i = n choose k ) )
thus ( len F = n + 1 & ( for i, k being Nat st i in dom F & k = i - 1 holds
F . i = n choose k ) ) by A2, FINSEQ_1:def 3; :: thesis: verum