let m, n be non zero Element of NAT ; :: thesis: for L being the carrier of () -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 () -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 S1[ 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 S1[i,y]
proof
let i be Nat; :: thesis: ( i in Seg m implies ex y being Element of BOOLEAN st S1[i,y] )
assume i in Seg m ; :: thesis: ex y being Element of BOOLEAN st S1[i,y]
then i in dom L by ;
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: S1[i,K . j]
thus S1[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
S1[i,x . i] ) ) from len x = m by ;
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 ; :: thesis: verum