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_{1}[ 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_{1}[i,y]

A3: ( dom x = Seg m & ( for i being Nat st i in Seg m holds

S_{1}[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

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

( 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

proof

consider x being FinSequence of BOOLEAN such that
let i be Nat; :: thesis: ( i in Seg m implies ex y being Element of BOOLEAN st S_{1}[i,y] )

assume i in Seg m ; :: thesis: ex y being Element of BOOLEAN st S_{1}[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_{1}[i,K . j]

thus S_{1}[i,K . j]
; :: thesis: verum

end;assume i in Seg m ; :: thesis: ex y being Element of BOOLEAN st S

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

thus S

A3: ( dom x = Seg m & ( for i being Nat st i in Seg m holds

S

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