for X being set
for S being SigmaField of X
for N, G being sequence of S ex F being sequence of S st
( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )