scheme :: STIRL2_1:sch 3
Sch3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅( object ) -> 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₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

provided

A1: for x being set st x in F₃() \ F₁() holds
F₅(x) in F₄() and
A2: ( F₁() c= F₃() & F₂() c= F₄() ) and
A3: ( F₂() is empty implies F₁() is empty ) and
A4: for f being Function of F₃(),F₄() st ( for x being set st x in F₃() \ F₁() holds
F₅(x) = f . x ) holds
( P₁[f,F₃(),F₄()] iff P₁[f | F₁(),F₁(),F₂()] )