thus ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) from :: thesis: for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (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 F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) implies x = y )

assume A1: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) ; :: thesis: ( for p being FinSequence holds
( not y = p . (len p) or not len p = len F1() or not p . 1 = F1() . 1 or ex k being Nat st
( 1 <= k & k < len F1() & not p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) or x = y )

assume A2: ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) ; :: thesis: x = y
thus x = y from :: thesis: verum