scheme :: LFUZZY_0:sch 3
FraenkelF9R9{ F₁() -> non empty set , F₂() -> non empty set , F₃( set , set ) -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

{ F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } = { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] }

provided

A1: for u being Element of F₁()
for v being Element of F₂() st P₁[u,v] holds
F₃(u,v) = F₄(u,v)