scheme :: STIRL2_1:sch 4
Sch4{ F₁() -> set , F₂() -> set , F₃() -> object , F₄() -> object , P₁[ set , set , set ] } :

card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of (F₁() \/ {F₃()}),(F₂() \/ {F₄()}) : ( P₁[f,F₁() \/ {F₃()},F₂() \/ {F₄()}] & rng (f | F₁()) c= F₂() & f . F₃() = F₄() ) }

provided

A1: ( F₂() is empty implies F₁() is empty ) and
A2: not F₃() in F₁() and
A3: for f being Function of (F₁() \/ {F₃()}),(F₂() \/ {F₄()}) st f . F₃() = F₄() holds
( P₁[f,F₁() \/ {F₃()},F₂() \/ {F₄()}] iff P₁[f | F₁(),F₁(),F₂()] )