let a be non empty FinSequence of REAL ; :: thesis: for Alg being Function of [:REAL,(NAT *):],NAT ex h being non empty FinSequence of NAT * st
( len h = len a & h . 1 = <*1*> & ( for i being Nat st 1 <= i & i < len a holds
ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = h . i & h . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) )
let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: ex h being non empty FinSequence of NAT * st
( len h = len a & h . 1 = <*1*> & ( for i being Nat st 1 <= i & i < len a holds
ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = h . i & h . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) )
defpred S₁[ object , object , object ] means ex d0 being Element of NAT ex d1 being Element of REAL ex d2 being Element of NAT * st
( $1 = d0 & d1 = a . (d0 + 1) & $2 = d2 & $3 = d2 ^ <*(Alg . (d1,d2))*> );
reconsider I1 = <*1*> as Element of NAT * by FINSEQ_1:def 11;
A1: for n0 being Nat st 1 <= n0 & n0 < len a holds
for f being Element of NAT * ex y being Element of NAT * st S₁[n0,f,y]

proof

let n0 be Nat; :: thesis: ( 1 <= n0 & n0 < len a implies for f being Element of NAT * ex y being Element of NAT * st S₁[n0,f,y] )
assume L01: ( 1 <= n0 & n0 < len a ) ; :: thesis: for f being Element of NAT * ex y being Element of NAT * st S₁[n0,f,y]
let f be Element of NAT * ; :: thesis: ex y being Element of NAT * st S₁[n0,f,y]
n0 + 1 <= len a by L01, NAT_1:13;
then L018: Seg (n0 + 1) c= Seg (len a) by FINSEQ_1:5;
n0 + 1 in Seg (len a) by L018, FINSEQ_1:3;
then n0 + 1 in dom a by FINSEQ_1:def 3;
then a . (n0 + 1) in rng a by FUNCT_1:3;
then reconsider dd1 = a . (n0 + 1) as Element of REAL ;
reconsider L = Alg . (dd1,f) as Element of NAT ;
reconsider y = f ^ <*L*> as Element of NAT * by FINSEQ_1:def 11;
FC99: ex d0 being Element of NAT ex d1 being Element of REAL ex d2 being Element of NAT * st
( n0 = d0 & d1 = a . (d0 + 1) & f = d2 & y = d2 ^ <*(Alg . (d1,d2))*> )

proof

reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
take n0 ; :: thesis: ex d1 being Element of REAL ex d2 being Element of NAT * st
( n0 = n0 & d1 = a . (n0 + 1) & f = d2 & y = d2 ^ <*(Alg . (d1,d2))*> )
take dd1 ; :: thesis: ex d2 being Element of NAT * st
( n0 = n0 & dd1 = a . (n0 + 1) & f = d2 & y = d2 ^ <*(Alg . (dd1,d2))*> )
take f ; :: thesis: ( n0 = n0 & dd1 = a . (n0 + 1) & f = f & y = f ^ <*(Alg . (dd1,f))*> )
thus ( n0 = n0 & dd1 = a . (n0 + 1) & f = f & y = f ^ <*(Alg . (dd1,f))*> ) ; :: thesis: verum

end;

take y ; :: thesis: S₁[n0,f,y]
thus S₁[n0,f,y] by FC99; :: thesis: verum

end;

consider H being FinSequence of NAT * such that
A2: ( len H = len a & ( H . 1 = I1 or len a = 0 ) & ( for n being Nat st 1 <= n & n < len a holds
S₁[n,H . n,H . (n + 1)] ) ) from RECDEF_1:sch 4(A1);
reconsider H = H as non empty FinSequence of NAT * by A2;
take H ; :: thesis: ( len H = len a & H . 1 = <*1*> & ( for i being Nat st 1 <= i & i < len a holds
ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = H . i & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) )
thus ( len H = len a & H . 1 = <*1*> ) by A2; :: thesis: for i being Nat st 1 <= i & i < len a holds
ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = H . i & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> )
thus for i being Nat st 1 <= i & i < len a holds
ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = H . i & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i < len a implies ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = H . i & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) )
assume ( 1 <= i & i < len a ) ; :: thesis: ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = H . i & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> )
then ex d0 being Element of NAT ex d1 being Element of REAL ex d2 being Element of NAT * st
( i = d0 & d1 = a . (d0 + 1) & H . i = d2 & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) by A2;
hence ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (i + 1) & d2 = H . i & H . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ; :: thesis: verum

end;