:: $n$-dimensional Binary Vector Spaces
:: by Kenichi Arai and Hiroyuki Okazaki
::
:: Received April 17, 2013
:: Copyright (c) 2013-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NBVECTSP, DESCIP_1, TARSKI, XBOOLE_0, FINSEQ_1, RELAT_1, FUNCT_1,
ARYTM_1, FUNCT_2, FINSEQ_2, NAT_1, XBOOLEAN, MARGREL1, ZFMISC_1,
SUBSET_1, NUMBERS, CARD_1, XXREAL_0, PARTFUN1, ARYTM_3, XCMPLX_0,
VALUED_1, FUNCOP_1, ALGSTR_0, STRUCT_0, RLVECT_1, SUPINF_2, MESFUNC1,
BINOP_1, VECTSP_1, RLSUB_1, RLVECT_5, RLVECT_2, CARD_3, FUNCT_4,
FINSET_1, RLVECT_3, BSPACE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FINSET_1, CARD_1, NUMBERS,
XXREAL_0, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCOP_1, XBOOLEAN,
MARGREL1, BINARITH, DESCIP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, MATRLIN, VECTSP_9, BSPACE;
constructors FINSEQ_1, RELSET_1, REAL_1, FINSEQ_4, NAT_D, FINSEQ_6, BINARITH,
DESCIP_1, BINARI_3, FUNCT_2, EUCLID, BINOP_1, XXREAL_0, NAT_1, RLVECT_1,
FINSEQ_2, GROUP_1, BINOP_2, MEMBERED, ARMSTRNG, XTUPLE_0, VECTSP_1,
VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, REALSET1, WAYBEL_4,
BSPACE;
registrations FINSEQ_1, RELSET_1, FINSEQ_2, ORDINAL1, FINSET_1, MARGREL1,
NAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, DESCIP_1, STRUCT_0, VECTSP_1,
FUNCOP_1, XBOOLEAN, FUNCT_4, VECTSP_9, FINSEQ_3, CARD_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM;
definitions ALGSTR_0, RLVECT_1, VECTSP_1;
equalities FINSEQ_1, FINSEQ_2, VECTSP_1, VECTSP_6, ALGSTR_0, STRUCT_0,
MARGREL1, XBOOLEAN;
expansions MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FUNCT_2, XXREAL_0, NAT_1, FINSEQ_1,
CARD_1, BINOP_1, FINSEQ_2, XBOOLEAN, XBOOLE_0, XBOOLE_1, DESCIP_1,
WELLORD2, RLVECT_2, FUNCOP_1, MARGREL1, RLVECT_1, ALGSTR_0, STRUCT_0,
VECTSP_4, VECTSP_6, MATRLIN, VECTSP_7, VECTSP_9, FUNCT_4, ORDINAL1,
BSPACE, VECTSP_1;
schemes FUNCT_1, FUNCT_2, FINSEQ_1, NAT_1, BINOP_1;
begin
reserve m,n,s for non zero Element of NAT;
Lm1:
for n be non zero Nat,
D be non empty set,
p be Element of n-tuples_on D
holds len p = n & p is Element of D*
proof
let n be non zero Nat,
D be non empty set,
p be Element of n-tuples_on D;
p in n-tuples_on D;
then ex s be Element of D* st p = s & len s = n;
hence thesis;
end;
theorem Th1:
for u1,v1,w1 be Element of n-tuples_on BOOLEAN
holds Op-XOR(Op-XOR(u1,v1),w1) = Op-XOR(u1,Op-XOR(v1,w1))
proof
let u1,v1,w1 be Element of n-tuples_on BOOLEAN;
A1: len Op-XOR(Op-XOR(u1,v1),w1) = n by Lm1;
A2: len Op-XOR(u1,Op-XOR(v1,w1)) = n by Lm1;
now let i be Nat;
assume 1 <= i & i <= len Op-XOR(Op-XOR(u1,v1),w1);
then
A3: i in Seg n by A1;
thus (Op-XOR(Op-XOR(u1,v1),w1)).i
= (Op-XOR(u1,v1)).i 'xor' w1.i by DESCIP_1:def 4,A3
.= (u1.i 'xor' v1.i) 'xor' w1.i by DESCIP_1:def 4,A3
.= u1.i 'xor' (v1.i 'xor' w1.i) by XBOOLEAN:73
.= u1.i 'xor' (Op-XOR(v1,w1)).i by DESCIP_1:def 4,A3
.= (Op-XOR(u1,Op-XOR(v1,w1))).i by DESCIP_1:def 4,A3;
end;
hence thesis by Lm1,A2,FINSEQ_1:14;
end;
definition
let n be non zero Element of NAT;
func XORB n -> BinOp of n-tuples_on BOOLEAN means
:Def1:
for x,y being Element of n-tuples_on BOOLEAN holds it.(x,y) = Op-XOR(x,y);
existence
proof
deffunc F(Element of n-tuples_on BOOLEAN,Element of n-tuples_on BOOLEAN)
= Op-XOR($1,$2);
consider f being Function of [:n-tuples_on BOOLEAN,n-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN such that
A1: for x,y being Element of n-tuples_on BOOLEAN
holds f.(x,y) = F(x,y) from BINOP_1:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
let H1,H2 be BinOp of n-tuples_on BOOLEAN;
assume
A2: for x,y be Element of n-tuples_on BOOLEAN
holds H1.(x,y) = Op-XOR(x,y);
assume
A3: for x,y be Element of n-tuples_on BOOLEAN
holds H2.(x,y) = Op-XOR(x,y);
for x,y be Element of n-tuples_on BOOLEAN
holds H1.(x,y) = H2.(x,y)
proof
let x,y be Element of n-tuples_on BOOLEAN;
thus H1.(x,y) = Op-XOR(x,y) by A2
.= H2.(x,y) by A3;
end;
hence H1 = H2 by BINOP_1:2;
end;
end;
definition
let n be non zero Element of NAT;
func ZeroB n -> Element of n-tuples_on BOOLEAN equals
n |-> 0;
correctness
proof
reconsider o = 0 as Element of BOOLEAN by TARSKI:def 2;
n |-> o in n-tuples_on BOOLEAN;
hence thesis;
end;
end;
definition
let n be non zero Element of NAT;
func n-BinaryGroup -> strict addLoopStr equals
addLoopStr(# n-tuples_on BOOLEAN, XORB n, ZeroB n #);
correctness;
end;
theorem Th2:
for u1 be Element of n-tuples_on BOOLEAN holds Op-XOR(u1,ZeroB n) = u1
proof
let u1 be Element of n-tuples_on BOOLEAN;
A1: len Op-XOR(u1,ZeroB n) = n by Lm1;
A2: len u1 = n by Lm1;
now let i be Nat;
assume 1 <= i & i <= len Op-XOR(u1,ZeroB n);
then
A3: i in Seg n by A1;
thus (Op-XOR(u1,ZeroB n)).i
= u1.i 'xor' (ZeroB n).i by DESCIP_1:def 4,A3
.= u1.i 'xor' FALSE
.= u1.i;
end;
hence thesis by Lm1,A2,FINSEQ_1:14;
end;
theorem Th3:
for u1 be Element of n-tuples_on BOOLEAN holds Op-XOR(u1,u1) = ZeroB n
proof
let u1 be Element of n-tuples_on BOOLEAN;
A1: len Op-XOR(u1,u1) = n by Lm1;
A2: len ZeroB n = n by Lm1;
now let i be Nat;
assume 1 <= i & i <= len Op-XOR(u1,u1); then
A3: i in Seg n by A1;
thus (Op-XOR(u1,u1)).i = u1.i 'xor' u1.i by DESCIP_1:def 4,A3
.= FALSE by XBOOLEAN:147
.= (ZeroB n).i;
end;
hence thesis by Lm1,A2,FINSEQ_1:14;
end;
registration
let n be non zero Element of NAT;
cluster n-BinaryGroup -> add-associative right_zeroed
right_complementable Abelian non empty;
coherence
proof
set IT = n-BinaryGroup;
hereby
let u,v,w be Element of IT;
reconsider u1 = u,v1 = v,w1 = w as Element of n-tuples_on BOOLEAN;
A1: u + v = Op-XOR(u1,v1) by Def1;
A2: v + w = Op-XOR(v1,w1) by Def1;
thus (u + v) + w = Op-XOR(Op-XOR(u1,v1),w1) by A1,Def1
.=Op-XOR(u1,Op-XOR(v1,w1)) by Th1
.=u + (v + w) by A2,Def1;
end;
hereby
let v be Element of IT;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
thus v + 0.IT = Op-XOR(v1,(ZeroB n)) by Def1
.=v by Th2;
end;
hereby
let v be Element of IT;
thus v is right_complementable
proof
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
take v;
thus v + v = Op-XOR(v1,v1) by Def1
.= 0.IT by Th3;
end;
end;
hereby
let u,v be Element of IT;
reconsider u1 = u,v1 = v as Element of n-tuples_on BOOLEAN;
thus u + v = Op-XOR(v1,u1) by Def1
.= v + u by Def1;
end;
thus thesis;
end;
end;
registration
cluster -> boolean for Element of Z_2;
coherence by BSPACE:3;
end;
registration
let u,v be Element of Z_2;
identify u + v with u 'xor' v;
compatibility
proof
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose u = 0.Z_2;
hence thesis by RLVECT_1:4,BSPACE:5;
end;
suppose
A1: u = 1.Z_2;
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose v = 0.Z_2;
hence thesis by RLVECT_1:4,BSPACE:5;
end;
suppose v = 1.Z_2;
hence thesis by A1,BSPACE:5,BSPACE:7,XBOOLEAN:147;
end;
end;
end;
identify u * v with u '&' v;
compatibility
proof
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose
A2: u = 0.Z_2;
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose v = 0.Z_2;
then u*v = (0.Z_2)*(0.Z_2)
.= 0 by BSPACE:5;
hence thesis by A2;
end;
suppose v = 1.Z_2;
u*v = (0.Z_2)*(1.Z_2) by A2
.= 0 by BSPACE:5;
hence thesis by A2;
end;
end;
suppose
A3: u = 1.Z_2;
per cases by BSPACE:5,BSPACE:6,XBOOLEAN:def 3;
suppose
A4: v = 0.Z_2;
then u*v = (1.Z_2)*(0.Z_2)
.= 0 by BSPACE:5;
hence thesis by A4;
end;
suppose v = 1.Z_2;
hence thesis by A3;
end;
end;
end;
end;
definition
let n be non zero Element of NAT;
func MLTB n -> Function of [:the carrier of Z_2,
n-tuples_on BOOLEAN:],n-tuples_on BOOLEAN means
:Def4:
for a be Element of BOOLEAN, x be Element of n-tuples_on BOOLEAN, i be set
st i in Seg n holds (it.(a,x)).i = a '&' x.i;
existence
proof
defpred P1[boolean object,boolean-valued Function,
boolean-valued Function] means
for i be set st i in Seg n holds $3.i = $1 '&' $2.i;
A1: for a being Element of BOOLEAN
for x being Element of n-tuples_on BOOLEAN
ex z being Element of n-tuples_on BOOLEAN st P1[a,x,z]
proof
let a be Element of BOOLEAN,
x be Element of n-tuples_on BOOLEAN;
deffunc H1(object) = a '&' (x.$1);
consider s being Function such that
A2: dom s = Seg n and
A3: for i being object st i in Seg n
holds s.i = H1(i) from FUNCT_1:sch 3;
A4: now let y be object;
assume y in rng s;
then consider i being object such that
A5: i in dom s and
A6: y = s.i by FUNCT_1:def 3;
y = a '&' (x.i) by A2, A3, A5, A6;
then (y = FALSE or y = TRUE) by XBOOLEAN:def 3;
hence y in BOOLEAN;
end;
reconsider s as boolean-valued Function by A4,TARSKI:def 3,
MARGREL1:def 16;
s is Function of Seg n,BOOLEAN by A2,FUNCT_2:2,TARSKI:def 3,A4;
then s is Element of Funcs ((Seg n),BOOLEAN) by FUNCT_2:8;
then reconsider s as Element of n-tuples_on BOOLEAN by FINSEQ_2:93;
for i being set st i in Seg n holds s.i = a '&' x.i by A3;
hence thesis;
end;
ex f being Function of [:BOOLEAN,n-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN st for a being Element of BOOLEAN
for x being Element of n-tuples_on BOOLEAN
holds P1[a,x,f.(a,x)] from BINOP_1:sch 3(A1);
hence thesis by BSPACE:3;
end;
uniqueness
proof
let f1,f2 be Function of [:the carrier of Z_2,
n-tuples_on BOOLEAN:],n-tuples_on BOOLEAN;
assume
A7: for a be Element of BOOLEAN,x be Element of n-tuples_on BOOLEAN
holds for i be set st i in Seg n holds (f1.(a,x)).i = a '&' x.i;
assume
A8: for a be Element of BOOLEAN, x be Element of n-tuples_on BOOLEAN
holds for i be set st i in Seg n
holds (f2.(a,x)).i = a '&' x.i;
now let a be Element of the carrier of Z_2,
x be Element of n-tuples_on BOOLEAN;
A9: len (f1.(a,x)) = n by CARD_1:def 7;
A10: len (f2.(a,x)) = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len (f1.(a,x)); then
A11: i in Seg n by A9;
thus (f1.(a,x)).i = a '&' x.i by A7,A11,BSPACE:3
.= (f2.(a,x)).i by A8,A11,BSPACE:3;
end;
hence f1.(a,x) = f2.(a,x) by FINSEQ_1:14,CARD_1:def 7,A10;
end;
hence f1 = f2 by BINOP_1:2;
end;
end;
definition
let n be non zero Element of NAT;
func n-BinaryVectSp -> VectSp of Z_2 equals
ModuleStr(# n-tuples_on BOOLEAN,XORB n,ZeroB n,MLTB n #);
correctness
proof
set X = Z_2;
set X0 = n-tuples_on BOOLEAN;
set Z0 = ZeroB n;
set ADD = XORB n;
set LMLT = MLTB n;
set XP = ModuleStr(# X0, ADD,Z0,LMLT #);
reconsider 1X = TRUE as Element of Z_2 by BSPACE:6;
A1: XP is scalar-distributive vector-distributive scalar-associative
scalar-unital
proof
thus XP is scalar-distributive
proof
let x,y be Element of X;
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider xyv1 = (x + y) * v as Element of n-tuples_on BOOLEAN;
reconsider xv = x * v as Element of n-tuples_on BOOLEAN;
reconsider yv = y * v as Element of n-tuples_on BOOLEAN;
reconsider xyv2 = x * v + y * v as Element of n-tuples_on BOOLEAN;
A2: len xyv1 = n by CARD_1:def 7;
A3: len xyv2 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len xyv1;
then
A4: i in Seg n by A2;
A5: xv.i = x '&' (v1.i) by Def4,A4,BSPACE:3;
A6: yv.i = y '&' (v1.i) by Def4,A4,BSPACE:3;
thus xyv1.i = (x 'xor' y) '&' (v1.i) by Def4,A4,BSPACE:3
.= xv.i 'xor' yv.i by XBOOLEAN:75,A5,A6
.= (Op-XOR(xv,yv)).i by DESCIP_1:def 4,A4
.= xyv2.i by Def1;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A3;
end;
thus XP is vector-distributive
proof
let x be Element of X;
let v,w be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider w1 = w as Element of n-tuples_on BOOLEAN;
reconsider xvw1 = x * (v + w) as Element of n-tuples_on BOOLEAN;
reconsider vw = v + w as Element of n-tuples_on BOOLEAN;
reconsider xv = x * v as Element of n-tuples_on BOOLEAN;
reconsider xw = x * w as Element of n-tuples_on BOOLEAN;
reconsider xvw2 = x * v + x * w as Element of n-tuples_on BOOLEAN;
A7: len xvw1 = n by CARD_1:def 7;
A8: len xvw2 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len xvw1;
then
A9: i in Seg n by A7;
A10: xv.i = x '&' (v1.i) by Def4,A9,BSPACE:3;
A11: xw.i = x '&' (w1.i) by Def4,A9,BSPACE:3;
A12: vw.i = (Op-XOR(v1,w1)).i by Def1
.= v1.i 'xor' w1.i by DESCIP_1:def 4,A9;
thus xvw2.i = (Op-XOR(xv,xw)).i by Def1
.= (x '&' (v1.i)) 'xor' (x '&' (w1.i)) by DESCIP_1:def 4,A9,A10,A11
.= x '&' (vw.i) by XBOOLEAN:75,A12
.= xvw1.i by Def4,A9,BSPACE:3;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A8;
end;
thus XP is scalar-associative
proof
let x,y be Element of X;
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider xyv1 = (x*y)*v as Element of n-tuples_on BOOLEAN;
reconsider yv1 = y*v as Element of n-tuples_on BOOLEAN;
reconsider xyv2 = x*(y*v) as Element of n-tuples_on BOOLEAN;
A13: len xyv1 = n by CARD_1:def 7;
A14: len xyv2 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len xyv1; then
A15: i in Seg n by A13;
A16: (yv1.i) = y '&' (v1.i) by Def4,A15,BSPACE:3;
thus xyv2.i = x '&' (yv1.i) by Def4,A15,BSPACE:3
.= (x '&' y) '&' (v1.i) by A16
.= xyv1.i by Def4,A15,BSPACE:3;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A14;
end;
thus XP is scalar-unital
proof
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
reconsider w1 = (MLTB n).(1X,v1) as Element of n-tuples_on BOOLEAN;
A17: len v1 = n by CARD_1:def 7;
A18: len w1 = n by CARD_1:def 7;
now let i be Nat;
assume 1 <= i & i <= len v1;
then i in Seg n by A17;
hence w1.i = TRUE '&' v1.i by Def4
.= v1.i;
end;
hence thesis by FINSEQ_1:14,CARD_1:def 7,A18,BSPACE:6;
end;
end;
A19: XP is add-associative
proof
for u,v,w being Element of XP holds (u + v) + w = u + (v + w)
proof
let u,v,w be Element of XP;
reconsider u1 = u,v1 = v,w1 = w as Element of n-tuples_on BOOLEAN;
A20: u + v = Op-XOR(u1,v1) by Def1;
A21: v + w = Op-XOR(v1,w1) by Def1;
thus (u + v) + w = Op-XOR(Op-XOR(u1,v1),w1) by A20,Def1
.= Op-XOR(u1,Op-XOR(v1,w1)) by Th1
.= u + (v + w) by A21,Def1;
end;
hence thesis by RLVECT_1:def 3;
end;
A22: XP is right_zeroed
proof
for v being Element of XP holds v + 0.XP = v
proof
let v be Element of XP;
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
thus v + 0.XP = Op-XOR(v1,(ZeroB n)) by Def1
.= v by Th2;
end;
hence thesis by RLVECT_1:def 4;
end;
A23: XP is right_complementable
proof
for x being Element of XP holds x is right_complementable
proof
let v be Element of XP;
ex y be Element of XP st v + y = 0.XP
proof
reconsider v1 = v as Element of n-tuples_on BOOLEAN;
take v;
thus v + v = Op-XOR(v1,v1) by Def1
.= 0.XP by Th3;
end;
hence thesis by ALGSTR_0:def 11;
end;
hence thesis by ALGSTR_0:def 16;
end;
XP is Abelian
proof
for v,w being Element of XP holds v + w = w + v
proof
let u,v be Element of XP;
reconsider u1 = u,v1 = v as Element of n-tuples_on BOOLEAN;
thus (u + v) = Op-XOR(v1,u1) by Def1
.= v + u by Def1;
end;
hence thesis by RLVECT_1:def 2;
end;
hence thesis by A1,A19,A22,A23;
end;
end;
registration
let n be non zero Element of NAT;
cluster n-BinaryVectSp -> finite;
coherence;
end;
registration
let n be non zero Element of NAT;
cluster -> finite for Subspace of n-BinaryVectSp;
coherence
proof
let V be Subspace of n-BinaryVectSp;
the carrier of V c= the carrier of n-BinaryVectSp by VECTSP_4:def 2;
hence thesis;
end;
end;
theorem Th4:
for n being Nat holds Sum(n|->0.Z_2) = 0.Z_2
proof
let n be Nat;
set x = n|->0.Z_2;
A1: len x = len x;
now let k be Nat;
assume k in dom x;
then x/.k = x.k by PARTFUN1:def 6
.= 0.Z_2 by BSPACE:5;
hence x.k = x/.k + x/.k by BSPACE:5;
end;
then
A2:Sum(x) - Sum(x) = Sum(x) + Sum(x) - Sum(x) by A1,RLVECT_2:2;
Sum(x) + Sum(x) - Sum(x) = Sum(x) + (Sum(x) - Sum(x)) by RLVECT_1:28
.= Sum(x) + 0.Z_2 by RLVECT_1:15
.= Sum(x) by BSPACE:5;
hence thesis by A2,RLVECT_1:15;
end;
theorem Th5:
for x be FinSequence of Z_2,
v be Element of Z_2,
j be Nat
st len x = m & j in Seg m & for i be Nat st i in Seg m holds
(i = j implies x.i = v) & (i <> j implies x.i = 0.Z_2)
holds Sum(x) = v
proof
defpred P[Nat] means
for m be non zero Element of NAT,
x be FinSequence of Z_2,
v be Element of Z_2,
j be Nat
st $1 = m & len x = m & j in Seg m & for i be Nat st i in Seg m holds
(i = j implies x.i = v) & (i <> j implies x.i = 0.Z_2)
holds Sum(x) = v;
A1: P[0];
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
for m be non zero Element of NAT, x be FinSequence of Z_2,
v be Element of Z_2, j be Nat
st k + 1 = m & len x = m & j in Seg m & for i be Nat st i in Seg m holds
(i = j implies x.i = v) & (i <> j implies x.i = 0.Z_2)
holds Sum(x) = v
proof
let m be non zero Element of NAT, x be FinSequence of Z_2,
v be Element of Z_2, j be Nat;
assume
A4: k + 1 = m & len x = m & j in Seg m & for i be Nat st i in Seg m holds
(i = j implies x.i = v) & (i <> j implies x.i = 0.Z_2);
reconsider xk = x|k as FinSequence of Z_2;
A5: k <= k + 1 by NAT_1:11;
A6: len xk = k by A4,NAT_1:11,FINSEQ_1:59;
A7: len x = len xk + 1 by A4,NAT_1:11,FINSEQ_1:59;
A8: xk = x | dom xk by A6,FINSEQ_1:def 3;
A9: len ((len xk)|->0.Z_2) = len xk by CARD_1:def 7;
per cases;
suppose
A10: j = m;
then
A11: x.(len x) = v by A4;
for i be Nat st i in dom xk holds xk.i = ((len xk)|->0.Z_2).i
proof
let i be Nat;
assume
A12: i in dom xk;
then
A13: i in Seg k by A6,FINSEQ_1:def 3;
then
A14: i in Seg m by A4,A5,FINSEQ_1:5,TARSKI:def 3;
1 <= i & i <= k by FINSEQ_1:1,A13;
then i <> j by A4,A10,NAT_1:13;
then x.i = 0.Z_2 by A4,A14;
then xk.i = 0.Z_2 by A12,A8,FUNCT_1:49;
hence thesis by BSPACE:5;
end; then
A15: xk = (len xk)|->0.Z_2 by A9,FINSEQ_2:9;
thus Sum(x) = Sum(xk) + v by RLVECT_1:38,A7,A8,A11
.= v + 0.Z_2 by A15,Th4
.= v by BSPACE:5;
end;
suppose
A16: j <> m;
A17: 1 <= j & j <= m by A4,FINSEQ_1:1;
then j < m by A16,XXREAL_0:1;
then j <= k by A4,NAT_1:13;
then
A18: j in Seg k by A17;
A19: k <> 0 by A4,A16,XXREAL_0:1,A17;
for i be Nat st i in Seg k holds (i = j implies xk.i = v) &
(i <> j implies xk.i = 0.Z_2)
proof
let i be Nat;
assume
A20: i in Seg k;
A21: Seg k c= Seg m by A4,NAT_1:11,FINSEQ_1:5;
xk.i = x.i by A20,FUNCT_1:49;
hence (i = j implies xk.i = v) &
(i <> j implies xk.i = 0.Z_2) by A4,A20,A21;
end;
then
A22: Sum(xk) = v by A6,A3,A18,A19;
A23: m in Seg m by FINSEQ_1:3;
A24: x.(len x) = 0.Z_2 by A4,A23,A16;
thus Sum(x) = v + 0.Z_2 by RLVECT_1:38,A7,A8,A24,A22
.= v by BSPACE:5;
end;
end;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th6:
for L be the carrier of (n-BinaryVectSp)-valued FinSequence,
j be Nat
st len L = m & m <= n & j in Seg n
ex x be FinSequence of Z_2 st len x = m &
for i be Nat st i in Seg m ex K be Element of n-tuples_on BOOLEAN
st K = L.i & x.i = K.j
proof
let L be the carrier of (n-BinaryVectSp)-valued FinSequence,
j be Nat;
assume
A1: len L = m & m <= n & j in Seg n;
defpred P1[Nat,set] means ex K be Element of n-tuples_on BOOLEAN
st K = L.$1 & $2 = K.j;
A2: for i be Nat st i in Seg m ex y being Element of BOOLEAN st P1[i,y]
proof
let i be Nat;
assume i in Seg m;
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;
thus P1[i,K.j];
end;
consider x being FinSequence of BOOLEAN such that
A3: dom x = Seg m & for i be Nat st i in Seg m holds P1[i,x.i]
from FINSEQ_1:sch 5 (A2);
len x = m by FINSEQ_1:def 3, A3;
hence thesis by A3,BSPACE:3;
end;
theorem Th7:
for L be the carrier of (n-BinaryVectSp)-valued FinSequence,
Suml be Element of n-tuples_on BOOLEAN,
j be Nat
st len L = m & m <= n & Suml = Sum(L) & j in Seg n
ex x be FinSequence of Z_2 st len x = m & (Suml).j = Sum(x) &
for i be Nat st i in Seg m ex K be Element of n-tuples_on BOOLEAN
st K = L.i & x.i = K.j
proof
let L be the carrier of (n-BinaryVectSp)-valued FinSequence,
Suml be Element of n-tuples_on BOOLEAN,
j be Nat;
assume
A1: len L = m & m <= n & Suml = Sum(L) & j in Seg n;
then consider x be FinSequence of Z_2 such that
A2: len x = m & for i be Nat st i in Seg m
ex K be 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 P1[Nat,set] means ex K be Element of n-tuples_on BOOLEAN
st K = f.$1 & $2 = K.j;
A4: for i be Element of NAT ex y being Element of the carrier of Z_2
st P1[i,y]
proof
let i be Element of NAT;
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;
thus P1[i,y];
end;
consider g being Function of NAT, Z_2 such that
A5: for i be Element of NAT holds P1[i,g.i] from FUNCT_2:sch 3 (A4);
set Sumlj = Suml.j;
A6: Sumlj = g.(len x)
proof
ex K be Element of n-tuples_on BOOLEAN st K = f.(len L) & g.(len L) = K.j
by A5;
hence Sumlj = g.(len x) by A1,A3,A2;
end;
A7: g.0 = 0.Z_2
proof
ex K be 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;
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, vj be Element of Z_2;
assume
A9: k < len x & vj = x.(k + 1);
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 be 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 be 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 be Nat holds P1[i,g.i]
proof
let i be Nat;
i is Element of NAT by ORDINAL1:def 12;
hence thesis by A5;
end; then
consider K0 be 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;
end;
(Suml).j = Sum(x) by A6,A7,A8,RLVECT_1:def 12;
hence thesis by A2;
end;
theorem Th8:
m <= n implies
ex A be FinSequence of n-tuples_on BOOLEAN st len A = m &
A is one-to-one & card (rng A) = m & (for i,j be Nat st i in Seg m &
j in Seg n holds (i = j implies (A.i).j = TRUE) &
(i <> j implies (A.i).j = FALSE))
proof
assume
A1: m <= n;
defpred P[Nat,Function] means for j be Nat st j in Seg n
holds ($1 = j implies $2.j = TRUE) & ($1 <> j implies $2.j = FALSE);
A2: for k be Nat st k in Seg m ex x being Element of n-tuples_on BOOLEAN
st P[k,x]
proof
let k be Nat;
assume k in Seg m;
defpred P1[Nat,set] means (k = $1 implies $2 = TRUE) &
(k <> $1 implies $2 = FALSE);
A3: for j be Nat st j in Seg n ex y being Element of BOOLEAN st P1[j,y]
proof
let j be Nat;
assume j in Seg n;
per cases;
suppose
A4: k = j;
take TRUE;
thus P1[j,TRUE] by A4;
end;
suppose
A5: k <> j;
take FALSE;
thus P1[j,FALSE] by A5;
end;
end;
consider x being FinSequence of BOOLEAN such that
A6: dom x = Seg n & for j be Nat st j in Seg n holds P1[j,x.j]
from FINSEQ_1:sch 5 (A3);
reconsider x as Element of (BOOLEAN)* by FINSEQ_1:def 11;
len x = n by A6,FINSEQ_1:def 3;
then x in {s where s is Element of BOOLEAN*: len s = n};
then reconsider x as Element of n-tuples_on BOOLEAN;
take x;
thus P[k,x] by A6;
end;
consider A being FinSequence of n-tuples_on BOOLEAN such that
A7: dom A = Seg m &
for k be Nat st k in Seg m holds P[k,A.k] from FINSEQ_1:sch 5 (A2);
take A;
thus len A = m by A7,FINSEQ_1:def 3;
A8: for x,y be object st x in dom A & y in dom A & A.x = A.y holds x = y
proof
let x,y be object;
assume
A9: x in dom A & y in dom A & A.x = A.y;
then reconsider i1 = x, i2 = y as Nat;
assume
A10: x <> y;
A11: Seg m c= Seg n by A1,FINSEQ_1:5;
(A.i2).i1 = FALSE by A10,A9,A7,A11;
hence contradiction by A9,A7,A11;
end;
hence A is one-to-one by FUNCT_1:def 4;
A12: card (dom A) = m by FINSEQ_1:57,A7;
dom A, rng A are_equipotent by A8,FUNCT_1:def 4,WELLORD2:def 4;
hence card (rng A) = m by A12,CARD_1:5;
thus thesis by A7;
end;
theorem Th9:
for A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp,
l being Linear_Combination of B,
Suml be Element of n-tuples_on BOOLEAN
st rng A = B & m <= n & len A = m & Suml = Sum l & A is one-to-one &
(for i,j be Nat st i in Seg n & j in Seg m holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
holds for j be Nat st j in Seg m holds (Suml).j = l.(A.j)
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp,
l be Linear_Combination of B,
Suml be Element of n-tuples_on BOOLEAN;
assume that
A1: rng A = B and
A2: m <= n and
A3: len A = m and
A4: Suml = Sum l and
A5: A is one-to-one and
A6: for i,j be Nat st i in Seg n & j in Seg m holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE);
set V = n-BinaryVectSp;
let j be Nat;
assume
A7: j in Seg m;
reconsider FA = A as FinSequence of V;
A8: j in Seg n by A7,A2,FINSEQ_1:5,TARSKI:def 3;
A9: Carrier l c= rng FA by A1,VECTSP_6:def 4;
A10: len (l (#) FA) = m by A3,VECTSP_6:def 5;
Suml = Sum (l (#) FA) by VECTSP_9:3,A5,A9,A4;
then consider x be FinSequence of Z_2 such that
A11: len x = m & (Suml).j = Sum(x) & for i be Nat st i in Seg m
ex K be Element of n-tuples_on BOOLEAN st K = (l (#) FA).i &
x.i = K.j by Th7,A2,A8,A10;
A12: for i be Nat st i in Seg m holds (i = j implies x.i = l.(A.j)) &
(i <> j implies x.i = 0.Z_2)
proof
let i be Nat;
assume
A13: i in Seg m;
then consider K be Element of n-tuples_on BOOLEAN such that
A14: K = (l (#) FA).i & x.i = K.j by A11;
A15: i in Seg n by A13,A2,FINSEQ_1:5,TARSKI:def 3;
A16: i in dom (l (#) FA) by FINSEQ_1:def 3,A13,A10;
A17: K = (l.(FA/.i)) * (FA/.i) by A14,A16,VECTSP_6:def 5;
reconsider FAi = (FA/.i) as Element of n-tuples_on BOOLEAN;
set lFAi = l.(FA/.i);
A18: K.j = lFAi '&' (FAi.j) by Def4,A8,A17,BSPACE:3;
A19: i in dom A by A3,FINSEQ_1:def 3,A13;
then
A20: FAi.j = (A.i).j by PARTFUN1:def 6;
thus i = j implies x.i = l.(A.j)
proof
assume
A21: i = j;
then K.j = lFAi '&' TRUE by A6,A8,A13,A18,A20;
hence x.i = l.(A.j) by A21,A14,A19,PARTFUN1:def 6;
end;
assume i <> j;
then K.j = lFAi '&' FALSE by A6,A7,A15,A18,A20;
hence x.i = 0.Z_2 by A14,BSPACE:5;
end;
j in dom A by A3,A7,FINSEQ_1:def 3;
then l.(A.j) is Element of Z_2 by PARTFUN1:4,FUNCT_2:5;
hence thesis by Th5,A7,A11,A12;
end;
theorem Th10:
for A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp
st rng A = B & m <= n & len A = m & A is one-to-one &
(for i,j be Nat st i in Seg n & j in Seg m holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
holds B is linearly-independent
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp;
assume that
A1: rng A = B and
A2: m <= n and
A3: len A = m and
A4: A is one-to-one and
A5: for i,j be Nat st i in Seg n & j in Seg m holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE);
set V = n-BinaryVectSp;
for l being Linear_Combination of B st Sum l = 0.V
holds Carrier l = {}
proof
let l be Linear_Combination of B;
assume
A6: Sum l = 0.V;
assume Carrier l <> {};
then consider x be object such that
A7: x in Carrier l by XBOOLE_0:def 1;
consider v be Element of V such that
A8: x = v & l.v <> 0.Z_2 by A7;
A9: Carrier l c= B by VECTSP_6:def 4;
reconsider Suml = Sum l as Element of n-tuples_on BOOLEAN;
consider j be object such that
A10: j in dom A & v = A.j by A1,A9,A7,A8,FUNCT_1:def 3;
A11: j in Seg m by A3,A10,FINSEQ_1:def 3;
reconsider j as Nat by A10;
(Suml).j = l.(A.j) by Th9,A1,A2,A3,A4,A5,A11;
hence contradiction by A6,A8,A10,BSPACE:5;
end;
hence thesis by VECTSP_7:def 1;
end;
theorem Th11:
for A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp,
v be Element of n-tuples_on BOOLEAN
st rng A = B & len A = n & A is one-to-one
ex l being Linear_Combination of B st
for j be Nat st j in Seg n holds v.j = l.(A.j)
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp,
v be Element of n-tuples_on BOOLEAN;
assume that
A1: rng A = B and
A2: len A = n and
A3: A is one-to-one;
set V = n-BinaryVectSp;
defpred P1[object,object] means ex j be Nat st j in Seg n &
$1 = A.j & $2 = v.j;
A4: for x being object st x in B ex y being object st
y in the carrier of Z_2 & P1[x,y]
proof
let x be object;
assume
A5: x in B;
consider j be object such that
A6: j in dom A & x = A.j by A1,A5,FUNCT_1:def 3;
A7: j in Seg n by A2,A6,FINSEQ_1:def 3;
reconsider j as Nat by A6;
v.j in the carrier of Z_2 by BSPACE:3;
hence thesis by A6,A7;
end;
consider l0 being Function of B,the carrier of Z_2 such that
A8: for x being object st x in B holds P1[x,l0.x] from FUNCT_2:sch 1(A4);
A9: for j be Nat st j in Seg n holds l0.(A.j) = v.j
proof
let j be Nat;
assume j in Seg n;
then
A10: j in dom A by A2,FINSEQ_1:def 3;
then consider i be Nat such that
A11: i in Seg n & A.j = A.i & l0.(A.j) = v.i by A1,FUNCT_1:3,A8;
i in dom A by A2,A11,FINSEQ_1:def 3;
hence l0.(A.j) = v.j by A3,A10,A11,FUNCT_1:def 4;
end;
set f = (the carrier of V) --> 0.Z_2;
set l = f +* l0;
A12: dom l = (dom f) \/ (dom l0) by FUNCT_4:def 1
.= (the carrier of V) \/ (dom l0)
.= (the carrier of V) \/ B by FUNCT_2:def 1
.= (the carrier of V) by XBOOLE_1:12;
rng l c= the carrier of Z_2;
then l is Function of (the carrier of V),the carrier of Z_2
by FUNCT_2:2,A12;
then reconsider l as Element of Funcs (the carrier of V,
the carrier of Z_2) by FUNCT_2:8;
A13: for v being Element of V st not v in B holds l.v = 0.Z_2
proof
let v be Element of V;
v in dom l by A12;
then
A14: v in (dom f) \/ (dom l0) by FUNCT_4:def 1;
assume not v in B;
then not v in dom l0;
then l.v = f.v by A14,FUNCT_4:def 1;
hence l.v = 0.Z_2;
end;
then reconsider l as Linear_Combination of V by VECTSP_6:def 1;
for x be object st x in Carrier l holds x in B
proof
let x be object;
assume x in Carrier l;
then ex v be Element of V st x = v & l.v <> 0.Z_2;
hence x in B by A13;
end;
then
A15: l is Linear_Combination of B by TARSKI:def 3,VECTSP_6:def 4;
for j be Nat st j in Seg n holds v.j = l.(A.j)
proof
let j be Nat;
assume
A16: j in Seg n;
then j in dom A by A2,FINSEQ_1:def 3;
then
A17: A.j in B by A1,FUNCT_1:3;
then reconsider x = A.j as Element of V;
A18: x in dom l0 by FUNCT_2:def 1,A17;
x in dom l by A12;
then
A19: x in (dom f) \/ (dom l0) by FUNCT_4:def 1;
thus l.(A.j) = l0.x by A18,A19,FUNCT_4:def 1
.= v.j by A9,A16;
end;
hence thesis by A15;
end;
theorem Th12:
for A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp
st rng A = B & len A = n & A is one-to-one &
(for i,j be Nat st i in Seg n & j in Seg n holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
holds Lin B = ModuleStr(# the carrier of n-BinaryVectSp,
the addF of n-BinaryVectSp, the ZeroF of n-BinaryVectSp,
the lmult of n-BinaryVectSp #)
proof
let A be FinSequence of n-tuples_on BOOLEAN,
B be finite Subset of n-BinaryVectSp;
assume that
A1: rng A = B and
A2: len A = n and
A3: A is one-to-one and
A4: for i,j be Nat st i in Seg n & j in Seg n
holds (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE);
set V = n-BinaryVectSp;
for x be object holds x in the carrier of (Lin B) iff x in the carrier of V
proof
let x be object;
hereby assume
A5: x in the carrier of Lin B;
the carrier of (Lin B) c= the carrier of V by VECTSP_4:def 2;
hence x in the carrier of V by A5;
end;
assume x in the carrier of V;
then reconsider v = x as Element of n-tuples_on BOOLEAN;
consider l being Linear_Combination of B such that
A6: for j be Nat st j in Seg n holds v.j = l.(A.j) by Th11,A1,A2,A3;
reconsider Suml = Sum l as Element of n-tuples_on BOOLEAN;
A7: len v = n by Lm1;
A8: len Suml = n by Lm1;
A9: dom v = Seg n by FINSEQ_1:def 3,A7
.= dom Suml by FINSEQ_1:def 3,A8;
for j be Nat st j in dom v holds v.j = Suml.j
proof
let j be Nat;
assume j in dom v;
then
A10: j in Seg n by FINSEQ_1:def 3,A7;
thus v.j = l.(A.j) by A6,A10
.= Suml.j by Th9,A1,A2,A3,A4,A10;
end;
then x in Lin B by FINSEQ_1:13,A9,VECTSP_7:7;
hence x in the carrier of (Lin B) by STRUCT_0:def 5;
end;
hence thesis by TARSKI:2,VECTSP_4:31;
end;
theorem Th13:
ex B be finite Subset of n-BinaryVectSp
st B is Basis of n-BinaryVectSp & card B = n &
ex A be FinSequence of n-tuples_on BOOLEAN st len A = n &
A is one-to-one & card (rng A) = n & rng A = B &
(for i,j be Nat st i in Seg n & j in Seg n holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
proof
set V = n-BinaryVectSp;
consider A be FinSequence of n-tuples_on BOOLEAN such that
A1: len A = n & A is one-to-one & card (rng A) = n &
(for i,j be Nat st i in Seg n & j in Seg n holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE))
by Th8;
reconsider B = rng A as finite Subset of n-BinaryVectSp;
A2: B is linearly-independent by A1,Th10;
Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V,
the lmult of V #) by A1,Th12;
then B is Basis of V by VECTSP_7:def 3,A2;
hence thesis by A1;
end;
theorem Th14:
n-BinaryVectSp is finite-dimensional & dim (n-BinaryVectSp) = n
proof
set V = n-BinaryVectSp;
consider B be finite Subset of n-BinaryVectSp such that
A1: B is Basis of n-BinaryVectSp & card B = n &
ex A be FinSequence of n-tuples_on BOOLEAN
st len A = n & A is one-to-one & card (rng A) = n & rng A = B &
for i,j be Nat st i in Seg n & j in Seg n
holds (i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE)
by Th13;
thus V is finite-dimensional by A1,MATRLIN:def 1;
hence dim V = n by A1,VECTSP_9:def 1;
end;
registration
let n be non zero Element of NAT;
cluster n-BinaryVectSp -> finite-dimensional;
coherence by Th14;
end;
theorem
for A be FinSequence of n-tuples_on BOOLEAN,
C be Subset of n-BinaryVectSp
st len A = n & A is one-to-one & card rng A = n &
(for i,j be Nat st i in Seg n & j in Seg n holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE)) &
C c= rng A
holds Lin C is Subspace of n-BinaryVectSp & C is Basis of Lin C &
dim (Lin C) = card C
proof
let A be FinSequence of n-tuples_on BOOLEAN,
C be Subset of n-BinaryVectSp;
assume
A1: len A = n & A is one-to-one & card rng A = n &
(for i,j be Nat st i in Seg n & j in Seg n holds
(i = j implies (A.i).j = TRUE) & (i <> j implies (A.i).j = FALSE));
assume
A2: C c= rng A;
reconsider B = rng A as finite Subset of n-BinaryVectSp;
B is linearly-independent by A1,Th10;
then
A3: C is linearly-independent by A2,VECTSP_7:1;
for x be object st x in C holds x in the carrier of Lin C
by VECTSP_7:8,STRUCT_0:def 5;
then reconsider C0 = C as Subset of (Lin C) by TARSKI:def 3;
Lin C0 = the ModuleStr of (Lin C) by VECTSP_9:17;
then C0 is Basis of Lin C by VECTSP_7:def 3,A3,VECTSP_9:12;
hence thesis by VECTSP_9:def 1;
end;