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

A5: for i being Element of NAT holds S_{1}[i,g . i]
from FUNCT_2:sch 3(A4);

set Sumlj = Suml . j;

A6: Suml . j = g . (len x)

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

g . (k + 1) = (g . k) + vj

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

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

( 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

proof

consider g being Function of NAT,Z_2 such that
let i be Element of NAT ; :: thesis: ex y being Element of the carrier of Z_2 st S_{1}[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_{1}[i,y]

thus S_{1}[i,y]
; :: thesis: verum

end;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

thus S

A5: for i being Element of NAT holds S

set Sumlj = Suml . j;

A6: Suml . j = g . (len x)

proof

A7:
g . 0 = 0. Z_2
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;( K = f . (len L) & g . (len L) = K . j ) by A5;

hence Suml . j = g . (len x) by A1, A3, A2; :: thesis: verum

proof

A8:
for k being Nat
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;( K = f . 0 & g . 0 = K . j ) by A5;

hence g . 0 = 0. Z_2 by A3, BSPACE:5; :: thesis: verum

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

g . (k + 1) = (g . k) + vj

proof

Suml . j = Sum x
by A6, A7, A8, RLVECT_1:def 12;
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_{1}[i,g . i]

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;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

proof

then consider K0 being Element of n -tuples_on BOOLEAN such that
let i be Nat; :: thesis: S_{1}[i,g . i]

i is Element of NAT by ORDINAL1:def 12;

hence S_{1}[i,g . i]
by A5; :: thesis: verum

end;i is Element of NAT by ORDINAL1:def 12;

hence S

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

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