A1: P₁[F₁()] and
A2: len F₁() = len F₂() and
A3: for p, q being FinSequence
for z1, z2 being set st P₁[(p ^ <*z1*>) ^ q] & P₂[z1,z2] holds
P₁[(p ^ <*z2*>) ^ q] and
A4: for i being Element of NAT st i in dom F₁() holds
P₂[F₁() . i,F₂() . i]