scheme :: MSAFREE4:sch 2
Sch2{ F1() -> non empty set , F2() -> V5() ManySortedSet of F1(), F3() -> V5() ManySortedSet of F1(), F4( object , object ) -> set } :
ex f being ManySortedFunction of F2(),F3() st
for i being Element of F1()
for a being Element of F2() . i holds (f . i) . a = F4(i,a)
provided
A1: for i being Element of F1()
for a being Element of F2() . i holds F4(i,a) in F3() . i