defpred S₁[ Nat, set ] means ex xi being Element of 8 -tuples_on BOOLEAN st
( xi = x . $1 & $2 = SBT . xi );
P1: for k being Nat st k in Seg 4 holds
ex z being Element of 8 -tuples_on BOOLEAN st S₁[k,z]

proof

let k be Nat; :: thesis: ( k in Seg 4 implies ex z being Element of 8 -tuples_on BOOLEAN st S₁[k,z] )
assume AS: k in Seg 4 ; :: thesis: ex z being Element of 8 -tuples_on BOOLEAN st S₁[k,z]
x in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then ex s being Element of (8 -tuples_on BOOLEAN) * st
( x = s & len s = 4 ) ;
then k in dom x by FINSEQ_1:def 3, AS;
then x . k in rng x by FUNCT_1:3;
then reconsider xk = x . k as Element of 8 -tuples_on BOOLEAN ;
SBT . xk is Element of 8 -tuples_on BOOLEAN ;
hence ex z being Element of 8 -tuples_on BOOLEAN st S₁[k,z] ; :: thesis: verum

end;

consider p being FinSequence of 8 -tuples_on BOOLEAN such that
P3: ( dom p = Seg 4 & ( for k being Nat st k in Seg 4 holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(P1);
reconsider p = p as Element of (8 -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
len p = 4 by P3, FINSEQ_1:def 3;
then p in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then reconsider p = p as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
take p ; :: thesis: for i being Element of Seg 4 holds p . i = SBT . (x . i)

now :: thesis: for i being Element of Seg 4 holds p . i = SBT . (x . i)

let i be Element of Seg 4; :: thesis: p . i = SBT . (x . i)
ex xi being Element of 8 -tuples_on BOOLEAN st
( xi = x . i & p . i = SBT . xi ) by P3;
hence p . i = SBT . (x . i) ; :: thesis: verum

end;

hence for i being Element of Seg 4 holds p . i = SBT . (x . i) ; :: thesis: verum