defpred S₁[ Nat, object ] means ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = $1 & $2 = (s . k) . m );
A1: for n being Element of NAT ex y being Element of D st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of D st S₁[n,y]
consider k, m being Nat such that
A2: ( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n ) by Th8;
(s . k) . m in rng (s . k) by A2, FUNCT_1:3;
then reconsider y = (s . k) . m as Element of D ;
take y ; :: thesis: S₁[n,y]
thus S₁[n,y] by A2; :: thesis: verum

end;

consider IT being Function of NAT,D such that
A4: for n being Element of NAT holds S₁[n,IT . n] from FUNCT_2:sch 3(A1);
reconsider IT = IT as sequence of D ;
take IT ; :: thesis: for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & IT . n = (s . k) . m )

hereby :: thesis: verum

let n be Nat; :: thesis: ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & IT . n = (s . k) . m )
n is Element of NAT by ORDINAL1:def 12;
hence ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & IT . n = (s . k) . m ) by A4; :: thesis: verum

end;