let m, n be non zero Element of NAT ; :: thesis: for L being the carrier of (n -BinaryVectSp) -valued FinSequence
for j being Nat st len L = m & m <= n & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) )
let L be the carrier of (n -BinaryVectSp) -valued FinSequence; :: thesis: for j being Nat st len L = m & m <= n & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) )
let j be Nat; :: thesis: ( len L = m & m <= n & j in Seg n implies ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) ) )
assume A1: ( len L = m & m <= n & j in Seg n ) ; :: thesis: ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) )
defpred S₁[ Nat, set ] means ex K being Element of n -tuples_on BOOLEAN st
( K = L . $1 & $2 = K . j );
A2: for i being Nat st i in Seg m holds
ex y being Element of BOOLEAN st S₁[i,y]

proof

let i be Nat; :: thesis: ( i in Seg m implies ex y being Element of BOOLEAN st S₁[i,y] )
assume i in Seg m ; :: thesis: ex y being Element of BOOLEAN st S₁[i,y]
then i in dom L by A1, FINSEQ_1:def 3;
then L /. i = L . i by PARTFUN1:def 6;
then reconsider K = L . i as Element of n -tuples_on BOOLEAN ;
take K . j ; :: thesis: S₁[i,K . j]
thus S₁[i,K . j] ; :: thesis: verum

end;

consider x being FinSequence of BOOLEAN such that
A3: ( dom x = Seg m & ( for i being Nat st i in Seg m holds
S₁[i,x . i] ) ) from FINSEQ_1:sch 5(A2);
len x = m by FINSEQ_1:def 3, A3;
hence ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) ) by A3, BSPACE:3; :: thesis: verum