scheme :: CFCONT_1:sch 1
CompSeqChoice{ P₁[ object , object ] } :

ex s1 being Complex_Sequence st
for n being Nat holds P₁[n,s1 . n]

provided

A1: for n being Nat ex g being Complex st P₁[n,g]