thus ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) from RECDEF_1:sch 6(); :: thesis: for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) holds
x = y
let x, y be set ; :: thesis: ( ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) implies x = y )
assume A1: ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) ; :: thesis: ( for p being FinSequence holds
( not y = p . (len p) or not len p = len F₁() or not p . 1 = F₁() . 1 or ex k being Nat st
( 1 <= k & k < len F₁() & not p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) or x = y )
assume A2: ex p being FinSequence st
( y = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) ; :: thesis: x = y
thus x = y from RECDEF_1:sch 10(A1, A2); :: thesis: verum