let F1, F2 be Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))); :: thesis: ( ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & F1 = p . (len N) ) & ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & F2 = p . (len N) ) implies F1 = F2 )
given p1 being FinSequence such that A32: ( len p1 = len N & p1 . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p1 . i & p1 . (i + 1) = NN * pp ) ) & F1 = p1 . (len N) ) ; :: thesis: ( for p being FinSequence holds
( not len p = len N or not p . 1 = N . 1 or ex i being Nat st
( 1 <= i & i < len N & ( for NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2)))
for pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) holds
( not NN = N . (i + 1) or not pp = p . i or not p . (i + 1) = NN * pp ) ) ) or not F2 = p . (len N) ) or F1 = F2 )
given p2 being FinSequence such that A33: ( len p2 = len N & p2 . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p2 . i & p2 . (i + 1) = NN * pp ) ) & F2 = p2 . (len N) ) ; :: thesis: F1 = F2
defpred S₁[ Nat, object , object ] means ex NN being Function of (REAL-NS (k . ($1 + 1))),(REAL-NS (k . ($1 + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . ($1 + 1))) st
( NN = N . ($1 + 1) & pp = $2 & $3 = NN * pp );
A34: ( len p1 = len N & ( p1 . 1 = N . 1 or len N = 0 ) & ( for i being Nat st 1 <= i & i < len N holds
S₁[i,p1 . i,p1 . (i + 1)] ) ) by A32;
A35: ( len p2 = len N & ( p2 . 1 = N . 1 or len N = 0 ) & ( for i being Nat st 1 <= i & i < len N holds
S₁[i,p2 . i,p2 . (i + 1)] ) ) by A33;
A36: for i being Nat st 1 <= i & i < len N holds
for x, y1, y2 being set st S₁[i,x,y1] & S₁[i,x,y2] holds
y1 = y2 ;
p1 = p2 from RECDEF_1:sch 7(A36, A34, A35);
hence F1 = F2 by A32, A33; :: thesis: verum