scheme :: DESCIP_1:sch 1
QuadChoiceRec{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅() -> Element of F₁(), F₆() -> Element of F₂(), F₇() -> Element of F₃(), F₈() -> Element of F₄(), P₁[ object , object , object , object , object , object , object , object , object ] } :

ex f being sequence of F₁() ex g being sequence of F₂() ex h being sequence of F₃() ex i being sequence of F₄() st
( f . 0 = F₅() & g . 0 = F₆() & h . 0 = F₇() & i . 0 = F₈() & ( for n being Element of NAT holds P₁[n,f . n,g . n,h . n,i . n,f . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) )

provided

A1: for n being Element of NAT
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for w being Element of F₄() ex x1 being Element of F₁() ex y1 being Element of F₂() ex z1 being Element of F₃() ex w1 being Element of F₄() st P₁[n,x,y,z,w,x1,y1,z1,w1]