defpred S₁[ set , set ] means ex i being Element of 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 13;
A2: for x being set st x in Seg n holds
ex y being set st S₁[x,y]

proof

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

end;

consider f being Function such that
A7: dom f = Seg n and
A8: for x being set 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 Element of 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 Element of NAT st i in dom f holds
f . i in Funcs (q . i),(q . (i + 1))
let i be Element of 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 Element of 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