set k = <*1,1*>;
rng <*1,1*> c= NAT by ORDINAL1:def 12;
then reconsider k = <*1,1*> as FinSequence of NAT by FINSEQ_1:def 4;
set N = <*(id the carrier of (REAL-NS 1))*>;
take <*(id the carrier of (REAL-NS 1))*> ; :: thesis: ex k being FinSequence of NAT st
( (len <*(id the carrier of (REAL-NS 1))*>) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
<*(id the carrier of (REAL-NS 1))*> . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) )
take k ; :: thesis: ( (len <*(id the carrier of (REAL-NS 1))*>) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
<*(id the carrier of (REAL-NS 1))*> . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) )
thus (len <*(id the carrier of (REAL-NS 1))*>) + 1 = 1 + 1 by FINSEQ_1:39
.= len k by FINSEQ_1:44 ; :: thesis: for i being Nat st 1 <= i & i < len k holds
<*(id the carrier of (REAL-NS 1))*> . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1)))
let i be Nat; :: thesis: ( 1 <= i & i < len k implies <*(id the carrier of (REAL-NS 1))*> . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) )
assume A1: ( 1 <= i & i < len k ) ; :: thesis: <*(id the carrier of (REAL-NS 1))*> . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1)))
then i < 1 + 1 by FINSEQ_1:44;
then i <= 1 by NAT_1:13;
then A2: i = 1 by A1, XXREAL_0:1;
thus <*(id the carrier of (REAL-NS 1))*> . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) by A2; :: thesis: verum