( 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₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) & ( 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₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) & 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₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) holds
x = y ) )

A1: for k being Nat
for y being set st 1 <= k & k < len F₁() holds
ex z being set st P₁[F₁() . (k + 1),y,z] and
A2: for k being Nat
for x, y1, y2, z being set st 1 <= k & k < len F₁() & z = F₁() . (k + 1) & P₁[z,x,y1] & P₁[z,x,y2] holds
y1 = y2