Rejestracja identyczności

registration
  let x1 be Θ1;
  .....
  let xn be Θn;
  identify (a1,...,ak)⊕(ak+1,...,am)
      with (b1,...,bj)⊗(bj+1,...,bs);
  reducibility
  proof
     thus (a1,...,ak)⊕(ak+1,...,am)
     = (b1,...,bj)⊗(bj+1,...,bs);
  end;
end;

Rejestracja identyczności powoduje utożsamienie (τ_a1,...,τ_ak)⊕(τ_ak+1,...,τ_am) z (τ_b1,...,τ_bj)⊗(τ_bj+1,...,τ_bs).