defpred S₁[ Nat, Element of R] 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 y being Element of R st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg (n + 1) implies ex y being Element of R st S₁[k,y] )
assume A2: k in Seg (n + 1) ; :: thesis: ex y being Element of R st S₁[k,y]
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;
reconsider z = ((n choose m1) * (a |^ l1)) * (b |^ m1) as Element of R ;
take z ; :: thesis: S₁[k,z]
thus S₁[k,z] ; :: thesis: verum

end;

consider p being FinSequence of the carrier of R such that
A3: ( dom p = Seg (n + 1) & ( for k being Nat st k in Seg (n + 1) holds
S₁[k,p /. k] ) ) from RECDEF_1:sch 17(A1);
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, FINSEQ_1:def 3; :: thesis: verum