defpred S₁[ object , object ] means ex i being Nat st
( i = $1 & $2 in Funcs ((q . i),(q . (i + 1))) );
consider n being Nat such that
A1: len q = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A2: for x being object st x in Seg n holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in Seg n implies ex y being object st S₁[x,y] )
assume A3: x in Seg n ; :: thesis: ex y being object st S₁[x,y]
then reconsider i = x as Nat ;
A4: i <= n by A3, FINSEQ_1:1;
then ( i + 1 >= 1 & i + 1 <= n + 1 ) by NAT_1:11, XREAL_1:6;
then A5: i + 1 in dom q by A1, FINSEQ_3:25;
n <= n + 1 by NAT_1:11;
then A6: i <= n + 1 by A4, XXREAL_0:2;
i >= 1 by A3, FINSEQ_1:1;
then i in dom q by A1, A6, FINSEQ_3:25;
then reconsider X = q . i, Y = q . (i + 1) as non empty set by A5;
set y = the Function of X,Y;
take the Function of X,Y ; :: thesis: S₁[x, the Function of X,Y]
take i ; :: thesis: ( i = x & the Function of X,Y in Funcs ((q . i),(q . (i + 1))) )
thus ( i = x & the Function of X,Y in Funcs ((q . i),(q . (i + 1))) ) by FUNCT_2:8; :: thesis: verum

end;

consider f being Function such that
A7: dom f = Seg n and
A8: for x being object st x in Seg n holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
reconsider f = f as FinSequence by A7, FINSEQ_1:def 2;
take f ; :: thesis: ( (len f) + 1 = len q & ( for i being Nat st i in dom f holds
f . i in Funcs ((q . i),(q . (i + 1))) ) )
thus (len f) + 1 = len q by A1, A7, FINSEQ_1:def 3; :: thesis: for i being Nat st i in dom f holds
f . i in Funcs ((q . i),(q . (i + 1)))
let i be Nat; :: thesis: ( i in dom f implies f . i in Funcs ((q . i),(q . (i + 1))) )
assume i in dom f ; :: thesis: f . i in Funcs ((q . i),(q . (i + 1)))
then ex j being Nat st
( j = i & f . i in Funcs ((q . j),(q . (j + 1))) ) by A7, A8;
hence f . i in Funcs ((q . i),(q . (i + 1))) ; :: thesis: verum