scheme :: INTEGR20:sch 1
ExRealSeq2X{ F₁() -> non empty set , F₂( set ) -> Element of F₁(), F₃( set ) -> Element of F₁() } :

ex s being sequence of F₁() st
for n being Nat holds
( s . (2 * n) = F₂(n) & s . ((2 * n) + 1) = F₃(n) )