let m, n be non zero Element of NAT ; :: thesis: for L being the carrier of (n -BinaryVectSp) -valued FinSequence
for Suml being Element of n -tuples_on BOOLEAN
for j being Nat st len L = m & m <= n & Suml = Sum L & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 Suml being Element of n -tuples_on BOOLEAN
for j being Nat st len L = m & m <= n & Suml = Sum L & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 Suml be Element of n -tuples_on BOOLEAN; :: thesis: for j being Nat st len L = m & m <= n & Suml = Sum L & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 & Suml = Sum L & j in Seg n implies ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 & Suml = Sum L & j in Seg n ) ; :: thesis: ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 ) ) )
then consider x being FinSequence of Z_2 such that
A2: ( 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 Th6;
consider f being Function of NAT,(n -BinaryVectSp) such that
A3: ( Sum L = f . (len L) & f . 0 = 0. (n -BinaryVectSp) & ( for j being Nat
for v being Element of (n -BinaryVectSp) st j < len L & v = L . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;
defpred S₁[ Nat, set ] means ex K being Element of n -tuples_on BOOLEAN st
( K = f . $1 & $2 = K . j );
A4: for i being Element of NAT ex y being Element of the carrier of Z_2 st S₁[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of the carrier of Z_2 st S₁[i,y]
reconsider K = f . i as Element of n -tuples_on BOOLEAN ;
reconsider y = K . j as Element of Z_2 by BSPACE:3;
take y ; :: thesis: S₁[i,y]
thus S₁[i,y] ; :: thesis: verum

end;

consider g being Function of NAT,Z_2 such that
A5: for i being Element of NAT holds S₁[i,g . i] from FUNCT_2:sch 3(A4);
set Sumlj = Suml . j;
A6: Suml . j = g . (len x)

proof

ex K being Element of n -tuples_on BOOLEAN st
( K = f . (len L) & g . (len L) = K . j ) by A5;
hence Suml . j = g . (len x) by A1, A3, A2; :: thesis: verum

end;

A7: g . 0 = 0. Z_2

proof

ex K being Element of n -tuples_on BOOLEAN st
( K = f . 0 & g . 0 = K . j ) by A5;
hence g . 0 = 0. Z_2 by A3, BSPACE:5; :: thesis: verum

end;

A8: for k being Nat
for vj being Element of Z_2 st k < len x & vj = x . (k + 1) holds
g . (k + 1) = (g . k) + vj

proof

let k be Nat; :: thesis: for vj being Element of Z_2 st k < len x & vj = x . (k + 1) holds
g . (k + 1) = (g . k) + vj
let vj be Element of Z_2; :: thesis: ( k < len x & vj = x . (k + 1) implies g . (k + 1) = (g . k) + vj )
assume A9: ( k < len x & vj = x . (k + 1) ) ; :: thesis: g . (k + 1) = (g . k) + vj
then ( 1 <= k + 1 & k + 1 <= len x ) by NAT_1:11, NAT_1:13;
then k + 1 in Seg m by A2;
then consider LVn being Element of n -tuples_on BOOLEAN such that
A10: ( LVn = L . (k + 1) & x . (k + 1) = LVn . j ) by A2;
reconsider Vn = LVn as Element of (n -BinaryVectSp) ;
consider K1 being Element of n -tuples_on BOOLEAN such that
A11: ( K1 = f . (k + 1) & g . (k + 1) = K1 . j ) by A5;
reconsider VK1 = K1 as Element of (n -BinaryVectSp) ;
for i being Nat holds S₁[i,g . i]

proof

let i be Nat; :: thesis: S₁[i,g . i]
i is Element of NAT by ORDINAL1:def 12;
hence S₁[i,g . i] by A5; :: thesis: verum

end;

then consider K0 being Element of n -tuples_on BOOLEAN such that
A12: ( K0 = f . k & g . k = K0 . j ) ;
reconsider VK0 = K0 as Element of (n -BinaryVectSp) ;
VK0 + Vn = Op-XOR (K0,LVn) by Def1;
hence g . (k + 1) = (g . k) + vj by A11, A3, A9, A10, A1, A2, A12, DESCIP_1:def 4; :: thesis: verum

end;

Suml . j = Sum x by A6, A7, A8, RLVECT_1:def 12;
hence ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 A2; :: thesis: verum