let m, n be non zero Element of NAT ; :: thesis: for L being the carrier of () -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 () -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,() such that
A3: ( Sum L = f . (len L) & f . 0 = 0. () & ( for j being Nat
for v being Element of () st j < len L & v = L . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;
defpred S1[ 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 S1[i,y]
proof
let i be Element of NAT ; :: thesis: ex y being Element of the carrier of Z_2 st S1[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: S1[i,y]
thus S1[i,y] ; :: thesis: verum
end;
consider g being Function of NAT,Z_2 such that
A5: for i being Element of NAT holds S1[i,g . i] from 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 ; :: 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 ;
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 () ;
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 () ;
for i being Nat holds S1[i,g . i]
proof
let i be Nat; :: thesis: S1[i,g . i]
i is Element of NAT by ORDINAL1:def 12;
hence S1[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 () ;
VK0 + Vn = Op-XOR (K0,LVn) by Def1;
hence g . (k + 1) = (g . k) + vj by ; :: thesis: verum
end;
Suml . j = Sum x by ;
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