let a be non empty FinSequence of REAL ; :: thesis: for Alg being Function of [:REAL,(NAT *):],NAT
for f, y being non empty FinSequence of NAT * st len f = len a & f . 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 = f . i & f . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len y = len a & y . 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 = y . i & y . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) holds
f = y
let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: for f, y being non empty FinSequence of NAT * st len f = len a & f . 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 = f . i & f . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len y = len a & y . 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 = y . i & y . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) holds
f = y
let f, y be non empty FinSequence of NAT * ; :: thesis: ( len f = len a & f . 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 = f . i & f . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) & len y = len a & y . 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 = y . i & y . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) implies f = y )
assume that
B1: ( len f = len a & f . 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 = f . i & f . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) and
B2: ( len y = len a & y . 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 = y . i & y . (i + 1) = d2 ^ <*(Alg . (d1,d2))*> ) ) ) ; :: thesis: f = y
for k being Nat st k in dom f holds
f . k = y . k

proof

let k be Nat; :: thesis: ( k in dom f implies f . k = y . k )
assume B41: k in dom f ; :: thesis: f . k = y . k
then B42: ( 1 <= k & k <= len a ) by B1, FINSEQ_3:25;
defpred S₁[ Nat] means f . $1 = y . $1;
F1: S₁[1] by B1, B2;
F2: for j being Element of NAT st 1 <= j & j < len a & ( for j2 being Element of NAT st 1 <= j2 & j2 <= j holds
S₁[j2] ) holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j < len a & ( for j2 being Element of NAT st 1 <= j2 & j2 <= j holds
S₁[j2] ) implies S₁[j + 1] )
assume that
F21: ( 1 <= j & j < len a ) and
F22: for j2 being Element of NAT st 1 <= j2 & j2 <= j holds
S₁[j2] ; :: thesis: S₁[j + 1]
F23: ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (j + 1) & d2 = f . j & f . (j + 1) = d2 ^ <*(Alg . (d1,d2))*> ) by B1, F21;
F24: ex d1 being Element of REAL ex d2 being FinSequence of NAT st
( d1 = a . (j + 1) & d2 = y . j & y . (j + 1) = d2 ^ <*(Alg . (d1,d2))*> ) by B2, F21;
f . j = y . j by F21, F22;
hence S₁[j + 1] by F23, F24; :: thesis: verum

end;

for i being Element of NAT st 1 <= i & i <= len a holds
S₁[i] from INT_1:sch 8(F1, F2);
hence f . k = y . k by B41, B42; :: thesis: verum

end;

hence f = y by B1, B2, FINSEQ_2:9; :: thesis: verum