reconsider n = n as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat, object ] means for l, m being Nat st m = $1 - 1 & l = n - m holds
$2 = ((n choose m) * (a |^ l)) * (b |^ m);
A1: for k being Nat st k in Seg (n + 1) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (n + 1) implies ex x being object st S₁[k,x] )
assume A2: k in Seg (n + 1) ; :: thesis: ex x being object st S₁[k,x]
then k >= 1 by FINSEQ_1:1;
then reconsider m1 = k - 1 as Element of NAT by INT_1:5;
k <= n + 1 by A2, FINSEQ_1:1;
then k - 1 <= (n + 1) - 1 by XREAL_1:9;
then reconsider l1 = n - m1 as Element of NAT by INT_1:5;
take ((n choose m1) * (a |^ l1)) * (b |^ m1) ; :: thesis: S₁[k,((n choose m1) * (a |^ l1)) * (b |^ m1)]
thus S₁[k,((n choose m1) * (a |^ l1)) * (b |^ m1)] ; :: thesis: verum

end;

consider p being FinSequence such that
A3: dom p = Seg (n + 1) and
A4: for k being Nat st k in Seg (n + 1) holds
S₁[k,p . k] from FINSEQ_1:sch 1(A1);
rng p c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in REAL )
assume x in rng p ; :: thesis: x in REAL
then consider y being object such that
A5: y in dom p and
A6: x = p . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A5;
y >= 1 by A3, A5, FINSEQ_1:1;
then reconsider m1 = y - 1 as Element of NAT by INT_1:5;
y <= n + 1 by A3, A5, FINSEQ_1:1;
then y - 1 <= (n + 1) - 1 by XREAL_1:9;
then reconsider l1 = n - m1 as Element of NAT by INT_1:5;
p . y = ((n choose m1) * (a |^ l1)) * (b |^ m1) by A3, A4, A5;
then reconsider x = x as Real by A6;
x in REAL by XREAL_0:def 1;
hence x in REAL ; :: thesis: verum

end;

then reconsider p = p as FinSequence of REAL by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = n + 1 & ( for i, l, m being Nat st i in dom p & m = i - 1 & l = n - m holds
p . i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
thus ( len p = n + 1 & ( for i, l, m being Nat st i in dom p & m = i - 1 & l = n - m holds
p . i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) by A3, A4, FINSEQ_1:def 3; :: thesis: verum