scheme :: INDEX_1:sch 1
LambdaMSFr{ F₁() -> non empty set , F₂() -> ManySortedCategory of F₁(), F₃() -> ManySortedCategory of F₁(), F₄( object ) -> set } :

ex F being ManySortedFunctor of F₂(),F₃() st
for a being Element of F₁() holds F . a = F₄(a)

provided

A1: for a being Element of F₁() holds F₄(a) is Functor of F₂() . a,F₃() . a