scheme :: HILB10_3:sch 2
Eq{ F₁() -> Nat, P₁[ object ], P₂[ object ] } :

{ p where p is F₁() -element XFinSequence of NAT : P₁[p] } = { q where q is F₁() -element XFinSequence of NAT : P₂[q] }

provided

A1: for p being F₁() -element XFinSequence of NAT holds
( P₁[p] iff P₂[p] )