scheme :: MOEBIUS1:sch 1
LambdaNATC{ F1() -> Element of NAT , F2() -> set , F3( object ) -> set } :
ex f being sequence of F2() st
( f . 0 = F1() & ( for x being non zero Element of NAT holds f . x = F3(x) ) )
provided
A1: F1() in F2() and
A2: for x being non zero Element of NAT holds F3(x) in F2()