defpred S₁[ set , set ] means for k being Nat st k = $1 holds
ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = $2 );
A1: for x being set st x in NAT holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
then reconsider k = x as Element of NAT ;
defpred S₂[ set , set ] means for i being Nat st i = $1 holds
$2 = (seq1 . i) * (seq2 . (k -' i));
A2: for i being Nat st i in k + 1 holds
ex z being Element of REAL st S₂[i,z]

proof

let i be Nat; :: thesis: ( i in k + 1 implies ex z being Element of REAL st S₂[i,z] )
assume i in k + 1 ; :: thesis: ex z being Element of REAL st S₂[i,z]
take (seq1 . i) * (seq2 . (k -' i)) ; :: thesis: S₂[i,(seq1 . i) * (seq2 . (k -' i))]
thus S₂[i,(seq1 . i) * (seq2 . (k -' i))] ; :: thesis: verum

end;

consider Fr being XFinSequence of such that
A3: dom Fr = k + 1 and
A4: for i being Nat st i in k + 1 holds
S₂[i,Fr . i] from STIRL2_1:sch 5(A2);
take Sum Fr ; :: thesis: ( Sum Fr in REAL & S₁[x, Sum Fr] )
for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) by A4;
hence ( Sum Fr in REAL & S₁[x, Sum Fr] ) by A3, XREAL_0:def 1; :: thesis: verum

end;

consider seq3 being Real_Sequence such that
A5: for x being set st x in NAT holds
S₁[x,seq3 . x] from FUNCT_2:sch 1(A1);
for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = seq3 . k )

proof

let k be Nat; :: thesis: ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = seq3 . k )
k in NAT by ORDINAL1:def 12;
hence ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = seq3 . k ) by A5; :: thesis: verum

end;

hence ex b₁ being Real_Sequence st
for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₁ . k ) ; :: thesis: verum