scheme :: PROB_4:sch 1
LambdaSigmaSSeq{ F1() -> set , F2() -> SigmaField of F1(), F3( set ) -> Element of F2() } :
ex f being SetSequence of F2() st
for n being Element of NAT holds f . n = F3(n)