scheme :: MSUALG_6:sch 3
MSRLambdaU{ F1() -> set , F2() -> ManySortedSet of F1(), F3( object ) -> set } :
( ex R being ManySortedRelation of F2() st
for i being object st i in F1() holds
R . i = F3(i) & ( for R1, R2 being ManySortedRelation of F2() st ( for i being object st i in F1() holds
R1 . i = F3(i) ) & ( for i being object st i in F1() holds
R2 . i = F3(i) ) holds
R1 = R2 ) )
provided
A1: for i being set st i in F1() holds
F3(i) is Relation of (F2() . i),(F2() . i)