let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V st 0. GF <> 1. GF holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for A being Subset of V st 0. GF <> 1. GF holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

let A be Subset of V; :: thesis: ( 0. GF <> 1. GF implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )

assume A1: 0. GF <> 1. GF ; :: thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) :: thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) )

hence A <> {} ; :: thesis: A is linearly-closed

( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V ) by Lm1, Th5;

then A55: 0. V in A by A54;

A56: for a being Element of GF

for v being Element of V st v in A holds

a * v in A

v + u in A :: according to VECTSP_4:def 1 :: thesis: for b_{1} being Element of the carrier of GF

for b_{2} being Element of the carrier of V holds

( not b_{2} in A or b_{1} * b_{2} in A )_{1} being Element of the carrier of GF

for b_{2} being Element of the carrier of V holds

( not b_{2} in A or b_{1} * b_{2} in A )
by A56; :: thesis: verum

for A being Subset of V st 0. GF <> 1. GF holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for A being Subset of V st 0. GF <> 1. GF holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

let A be Subset of V; :: thesis: ( 0. GF <> 1. GF implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )

assume A1: 0. GF <> 1. GF ; :: thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) :: thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) )

proof

assume A54:
for l being Linear_Combination of A holds Sum l in A
; :: thesis: ( A <> {} & A is linearly-closed )
defpred S_{1}[ Nat] means for l being Linear_Combination of A st card (Carrier l) = $1 holds

Sum l in A;

assume that

A2: A <> {} and

A3: A is linearly-closed ; :: thesis: for l being Linear_Combination of A holds Sum l in A

A4: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]

A53: card (Carrier l) = card (Carrier l) ;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A5);

hence Sum l in A by A53; :: thesis: verum

end;Sum l in A;

assume that

A2: A <> {} and

A3: A is linearly-closed ; :: thesis: for l being Linear_Combination of A holds Sum l in A

A4: S

proof

A5:
for k being Nat st S
let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = 0 implies Sum l in A )

assume card (Carrier l) = 0 ; :: thesis: Sum l in A

then Carrier l = {} ;

then l = ZeroLC V by Def3;

then Sum l = 0. V by Lm1;

hence Sum l in A by A2, A3, VECTSP_4:1; :: thesis: verum

end;assume card (Carrier l) = 0 ; :: thesis: Sum l in A

then Carrier l = {} ;

then l = ZeroLC V by Def3;

then Sum l = 0. V by Lm1;

hence Sum l in A by A2, A3, VECTSP_4:1; :: thesis: verum

S

proof

let l be Linear_Combination of A; :: thesis: Sum l in A
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = k + 1 implies Sum l in A )

deffunc H_{1}( Element of V) -> Element of the carrier of GF = l . $1;

consider F being FinSequence of V such that

A7: F is one-to-one and

A8: rng F = Carrier l and

A9: Sum l = Sum (l (#) F) by Def6;

reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;

assume A10: card (Carrier l) = k + 1 ; :: thesis: Sum l in A

then A11: len F = k + 1 by A7, A8, FINSEQ_4:62;

then A12: len (l (#) F) = k + 1 by Def5;

A13: k + 1 in Seg (k + 1) by FINSEQ_1:4;

then A14: k + 1 in dom F by A11, FINSEQ_1:def 3;

k + 1 in dom F by A11, A13, FINSEQ_1:def 3;

then reconsider v = F . (k + 1) as Element of V by FINSEQ_2:11;

consider f being Function of the carrier of V, the carrier of GF such that

A15: f . v = 0. GF and

A16: for u being Element of V st u <> v holds

f . u = H_{1}(u)
from FUNCT_2:sch 6();

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

A17: v in Carrier l by A8, A14, FUNCT_1:def 3;

A19: A \ {v} c= A by XBOOLE_1:36;

A20: Carrier l c= A by Def4;

then A21: (l . v) * v in A by A3, A17;

A22: Carrier f = (Carrier l) \ {v}

then Carrier f c= A by A19;

then reconsider f = f as Linear_Combination of A by Def4;

A29: len G = k by A11, FINSEQ_3:53;

then A30: len (f (#) G) = k by Def5;

A31: rng G = Carrier f

.= dom (f (#) G) by A30, FINSEQ_1:def 3 ;

then A42: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A12, FINSEQ_1:def 3;

then A50: f (#) G = (l (#) F) | (dom (f (#) G)) by A30, FINSEQ_1:def 3;

v in rng F by A14, FUNCT_1:def 3;

then {v} c= Carrier l by A8, ZFMISC_1:31;

then card (Carrier f) = (k + 1) - (card {v}) by A10, A22, CARD_2:44

.= (k + 1) - 1 by CARD_1:30

.= k by XCMPLX_1:26 ;

then A51: Sum f in A by A6;

G is one-to-one by A7, FUNCT_1:52;

then A52: Sum (f (#) G) = Sum f by A31, Def6;

(l (#) F) . (len F) = (l . v) * v by A11, A14, Th8;

then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A11, A12, A30, A50, RLVECT_1:38;

hence Sum l in A by A3, A9, A21, A52, A51; :: thesis: verum

end;assume A6: S

let l be Linear_Combination of A; :: thesis: ( card (Carrier l) = k + 1 implies Sum l in A )

deffunc H

consider F being FinSequence of V such that

A7: F is one-to-one and

A8: rng F = Carrier l and

A9: Sum l = Sum (l (#) F) by Def6;

reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;

assume A10: card (Carrier l) = k + 1 ; :: thesis: Sum l in A

then A11: len F = k + 1 by A7, A8, FINSEQ_4:62;

then A12: len (l (#) F) = k + 1 by Def5;

A13: k + 1 in Seg (k + 1) by FINSEQ_1:4;

then A14: k + 1 in dom F by A11, FINSEQ_1:def 3;

k + 1 in dom F by A11, A13, FINSEQ_1:def 3;

then reconsider v = F . (k + 1) as Element of V by FINSEQ_2:11;

consider f being Function of the carrier of V, the carrier of GF such that

A15: f . v = 0. GF and

A16: for u being Element of V st u <> v holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

A17: v in Carrier l by A8, A14, FUNCT_1:def 3;

now :: thesis: for u being Element of V st not u in Carrier l holds

f . u = 0. GF

then reconsider f = f as Linear_Combination of V by Def1;f . u = 0. GF

let u be Element of V; :: thesis: ( not u in Carrier l implies f . u = 0. GF )

assume A18: not u in Carrier l ; :: thesis: f . u = 0. GF

hence f . u = l . u by A17, A16

.= 0. GF by A18 ;

:: thesis: verum

end;assume A18: not u in Carrier l ; :: thesis: f . u = 0. GF

hence f . u = l . u by A17, A16

.= 0. GF by A18 ;

:: thesis: verum

A19: A \ {v} c= A by XBOOLE_1:36;

A20: Carrier l c= A by Def4;

then A21: (l . v) * v in A by A3, A17;

A22: Carrier f = (Carrier l) \ {v}

proof

then
Carrier f c= A \ {v}
by A20, XBOOLE_1:33;
thus
Carrier f c= (Carrier l) \ {v}
:: according to XBOOLE_0:def 10 :: thesis: (Carrier l) \ {v} c= Carrier f

assume A26: x in (Carrier l) \ {v} ; :: thesis: x in Carrier f

then x in Carrier l by XBOOLE_0:def 5;

then consider u being Element of V such that

A27: x = u and

A28: l . u <> 0. GF ;

not x in {v} by A26, XBOOLE_0:def 5;

then x <> v by TARSKI:def 1;

then l . u = f . u by A16, A27;

hence x in Carrier f by A27, A28; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Carrier l) \ {v} or x in Carrier f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in (Carrier l) \ {v} )

assume x in Carrier f ; :: thesis: x in (Carrier l) \ {v}

then consider u being Element of V such that

A23: u = x and

A24: f . u <> 0. GF ;

f . u = l . u by A15, A16, A24;

then A25: x in Carrier l by A23, A24;

not x in {v} by A15, A23, A24, TARSKI:def 1;

hence x in (Carrier l) \ {v} by A25, XBOOLE_0:def 5; :: thesis: verum

end;assume x in Carrier f ; :: thesis: x in (Carrier l) \ {v}

then consider u being Element of V such that

A23: u = x and

A24: f . u <> 0. GF ;

f . u = l . u by A15, A16, A24;

then A25: x in Carrier l by A23, A24;

not x in {v} by A15, A23, A24, TARSKI:def 1;

hence x in (Carrier l) \ {v} by A25, XBOOLE_0:def 5; :: thesis: verum

assume A26: x in (Carrier l) \ {v} ; :: thesis: x in Carrier f

then x in Carrier l by XBOOLE_0:def 5;

then consider u being Element of V such that

A27: x = u and

A28: l . u <> 0. GF ;

not x in {v} by A26, XBOOLE_0:def 5;

then x <> v by TARSKI:def 1;

then l . u = f . u by A16, A27;

hence x in Carrier f by A27, A28; :: thesis: verum

then Carrier f c= A by A19;

then reconsider f = f as Linear_Combination of A by Def4;

A29: len G = k by A11, FINSEQ_3:53;

then A30: len (f (#) G) = k by Def5;

A31: rng G = Carrier f

proof

(Seg (k + 1)) /\ (Seg k) =
Seg k
by FINSEQ_1:7, NAT_1:12
thus
rng G c= Carrier f
:: according to XBOOLE_0:def 10 :: thesis: Carrier f c= rng G

assume A38: x in Carrier f ; :: thesis: x in rng G

then x in rng F by A8, A22, XBOOLE_0:def 5;

then consider y being object such that

A39: y in dom F and

A40: F . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A39, FINSEQ_3:23;

then A41: y in dom G by RELAT_1:61;

then G . y = F . y by FUNCT_1:47;

hence x in rng G by A40, A41, FUNCT_1:def 3; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in rng G )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in Carrier f )

assume x in rng G ; :: thesis: x in Carrier f

then consider y being object such that

A32: y in dom G and

A33: G . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A32, FINSEQ_3:23;

A34: ( dom G c= dom F & G . y = F . y ) by A32, FUNCT_1:47, RELAT_1:60;

x in rng F by A32, A33, A34, FUNCT_1:def 3;

hence x in Carrier f by A8, A22, A37, XBOOLE_0:def 5; :: thesis: verum

end;assume x in rng G ; :: thesis: x in Carrier f

then consider y being object such that

A32: y in dom G and

A33: G . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A32, FINSEQ_3:23;

A34: ( dom G c= dom F & G . y = F . y ) by A32, FUNCT_1:47, RELAT_1:60;

now :: thesis: not x = v

then A37:
not x in {v}
by TARSKI:def 1;assume
x = v
; :: thesis: contradiction

then A35: k + 1 = y by A7, A14, A32, A33, A34;

A36: k in NAT by ORDINAL1:def 12;

y <= k by A29, A32, FINSEQ_3:25;

hence contradiction by A35, XREAL_1:29, A36; :: thesis: verum

end;then A35: k + 1 = y by A7, A14, A32, A33, A34;

A36: k in NAT by ORDINAL1:def 12;

y <= k by A29, A32, FINSEQ_3:25;

hence contradiction by A35, XREAL_1:29, A36; :: thesis: verum

x in rng F by A32, A33, A34, FUNCT_1:def 3;

hence x in Carrier f by A8, A22, A37, XBOOLE_0:def 5; :: thesis: verum

assume A38: x in Carrier f ; :: thesis: x in rng G

then x in rng F by A8, A22, XBOOLE_0:def 5;

then consider y being object such that

A39: y in dom F and

A40: F . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A39, FINSEQ_3:23;

now :: thesis: y in Seg k

then
y in (dom F) /\ (Seg k)
by A39, XBOOLE_0:def 4;assume
not y in Seg k
; :: thesis: contradiction

then y in (dom F) \ (Seg k) by A39, XBOOLE_0:def 5;

then y in (Seg (k + 1)) \ (Seg k) by A11, FINSEQ_1:def 3;

then y in {(k + 1)} by FINSEQ_3:15;

then y = k + 1 by TARSKI:def 1;

then not v in {v} by A22, A38, A40, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then y in (dom F) \ (Seg k) by A39, XBOOLE_0:def 5;

then y in (Seg (k + 1)) \ (Seg k) by A11, FINSEQ_1:def 3;

then y in {(k + 1)} by FINSEQ_3:15;

then y = k + 1 by TARSKI:def 1;

then not v in {v} by A22, A38, A40, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

then A41: y in dom G by RELAT_1:61;

then G . y = F . y by FUNCT_1:47;

hence x in rng G by A40, A41, FUNCT_1:def 3; :: thesis: verum

.= dom (f (#) G) by A30, FINSEQ_1:def 3 ;

then A42: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A12, FINSEQ_1:def 3;

now :: thesis: for x being object st x in dom (f (#) G) holds

(f (#) G) . x = (l (#) F) . x

then
f (#) G = (l (#) F) | (Seg k)
by A42, FUNCT_1:46;(f (#) G) . x = (l (#) F) . x

let x be object ; :: thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )

A43: rng F c= the carrier of V by FINSEQ_1:def 4;

assume A44: x in dom (f (#) G) ; :: thesis: (f (#) G) . x = (l (#) F) . x

then reconsider n = x as Element of NAT by FINSEQ_3:23;

n in dom (l (#) F) by A42, A44, XBOOLE_0:def 4;

then A45: n in dom F by A11, A12, FINSEQ_3:29;

then F . n in rng F by FUNCT_1:def 3;

then reconsider w = F . n as Element of V by A43;

A46: n in dom G by A29, A30, A44, FINSEQ_3:29;

then A47: G . n in rng G by FUNCT_1:def 3;

rng G c= the carrier of V by FINSEQ_1:def 4;

then reconsider u = G . n as Element of V by A47;

not u in {v} by A22, A31, A47, XBOOLE_0:def 5;

then A48: u <> v by TARSKI:def 1;

A49: (f (#) G) . n = (f . u) * u by A46, Th8

.= (l . u) * u by A16, A48 ;

w = u by A46, FUNCT_1:47;

hence (f (#) G) . x = (l (#) F) . x by A49, A45, Th8; :: thesis: verum

end;A43: rng F c= the carrier of V by FINSEQ_1:def 4;

assume A44: x in dom (f (#) G) ; :: thesis: (f (#) G) . x = (l (#) F) . x

then reconsider n = x as Element of NAT by FINSEQ_3:23;

n in dom (l (#) F) by A42, A44, XBOOLE_0:def 4;

then A45: n in dom F by A11, A12, FINSEQ_3:29;

then F . n in rng F by FUNCT_1:def 3;

then reconsider w = F . n as Element of V by A43;

A46: n in dom G by A29, A30, A44, FINSEQ_3:29;

then A47: G . n in rng G by FUNCT_1:def 3;

rng G c= the carrier of V by FINSEQ_1:def 4;

then reconsider u = G . n as Element of V by A47;

not u in {v} by A22, A31, A47, XBOOLE_0:def 5;

then A48: u <> v by TARSKI:def 1;

A49: (f (#) G) . n = (f . u) * u by A46, Th8

.= (l . u) * u by A16, A48 ;

w = u by A46, FUNCT_1:47;

hence (f (#) G) . x = (l (#) F) . x by A49, A45, Th8; :: thesis: verum

then A50: f (#) G = (l (#) F) | (dom (f (#) G)) by A30, FINSEQ_1:def 3;

v in rng F by A14, FUNCT_1:def 3;

then {v} c= Carrier l by A8, ZFMISC_1:31;

then card (Carrier f) = (k + 1) - (card {v}) by A10, A22, CARD_2:44

.= (k + 1) - 1 by CARD_1:30

.= k by XCMPLX_1:26 ;

then A51: Sum f in A by A6;

G is one-to-one by A7, FUNCT_1:52;

then A52: Sum (f (#) G) = Sum f by A31, Def6;

(l (#) F) . (len F) = (l . v) * v by A11, A14, Th8;

then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A11, A12, A30, A50, RLVECT_1:38;

hence Sum l in A by A3, A9, A21, A52, A51; :: thesis: verum

A53: card (Carrier l) = card (Carrier l) ;

for k being Nat holds S

hence Sum l in A by A53; :: thesis: verum

hence A <> {} ; :: thesis: A is linearly-closed

( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V ) by Lm1, Th5;

then A55: 0. V in A by A54;

A56: for a being Element of GF

for v being Element of V st v in A holds

a * v in A

proof

thus
for v, u being Element of V st v in A & u in A holds
let a be Element of GF; :: thesis: for v being Element of V st v in A holds

a * v in A

let v be Element of V; :: thesis: ( v in A implies a * v in A )

assume A57: v in A ; :: thesis: a * v in A

end;a * v in A

let v be Element of V; :: thesis: ( v in A implies a * v in A )

assume A57: v in A ; :: thesis: a * v in A

now :: thesis: a * v in Aend;

hence
a * v in A
; :: thesis: verumper cases
( a = 0. GF or a <> 0. GF )
;

end;

suppose A58:
a <> 0. GF
; :: thesis: a * v in A

deffunc H_{1}( set ) -> Element of the carrier of GF = 0. GF;

consider f being Function of V,GF such that

A59: f . v = a and

A60: for u being Element of V st u <> v holds

f . u = H_{1}(u)
from FUNCT_2:sch 6();

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

A61: Carrier f = {v}

then reconsider f = f as Linear_Combination of A by A61, Def4;

consider F being FinSequence of V such that

A64: ( F is one-to-one & rng F = Carrier f ) and

A65: Sum (f (#) F) = Sum f by Def6;

F = <*v*> by A61, A64, FINSEQ_3:97;

then f (#) F = <*((f . v) * v)*> by Th10;

then Sum f = a * v by A59, A65, RLVECT_1:44;

hence a * v in A by A54; :: thesis: verum

end;consider f being Function of V,GF such that

A59: f . v = a and

A60: for u being Element of V st u <> v holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

now :: thesis: for u being Element of V st not u in {v} holds

f . u = 0. GF

then reconsider f = f as Linear_Combination of V by Def1;f . u = 0. GF

let u be Element of V; :: thesis: ( not u in {v} implies f . u = 0. GF )

assume not u in {v} ; :: thesis: f . u = 0. GF

then u <> v by TARSKI:def 1;

hence f . u = 0. GF by A60; :: thesis: verum

end;assume not u in {v} ; :: thesis: f . u = 0. GF

then u <> v by TARSKI:def 1;

hence f . u = 0. GF by A60; :: thesis: verum

A61: Carrier f = {v}

proof

{v} c= A
by A57, ZFMISC_1:31;
thus
Carrier f c= {v}
:: according to XBOOLE_0:def 10 :: thesis: {v} c= Carrier f

assume x in {v} ; :: thesis: x in Carrier f

then x = v by TARSKI:def 1;

hence x in Carrier f by A58, A59; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in Carrier f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )

assume x in Carrier f ; :: thesis: x in {v}

then consider u being Element of V such that

A62: x = u and

A63: f . u <> 0. GF ;

u = v by A60, A63;

hence x in {v} by A62, TARSKI:def 1; :: thesis: verum

end;assume x in Carrier f ; :: thesis: x in {v}

then consider u being Element of V such that

A62: x = u and

A63: f . u <> 0. GF ;

u = v by A60, A63;

hence x in {v} by A62, TARSKI:def 1; :: thesis: verum

assume x in {v} ; :: thesis: x in Carrier f

then x = v by TARSKI:def 1;

hence x in Carrier f by A58, A59; :: thesis: verum

then reconsider f = f as Linear_Combination of A by A61, Def4;

consider F being FinSequence of V such that

A64: ( F is one-to-one & rng F = Carrier f ) and

A65: Sum (f (#) F) = Sum f by Def6;

F = <*v*> by A61, A64, FINSEQ_3:97;

then f (#) F = <*((f . v) * v)*> by Th10;

then Sum f = a * v by A59, A65, RLVECT_1:44;

hence a * v in A by A54; :: thesis: verum

v + u in A :: according to VECTSP_4:def 1 :: thesis: for b

for b

( not b

proof

thus
for b
let v, u be Element of V; :: thesis: ( v in A & u in A implies v + u in A )

assume that

A66: v in A and

A67: u in A ; :: thesis: v + u in A

end;assume that

A66: v in A and

A67: u in A ; :: thesis: v + u in A

now :: thesis: v + u in Aend;

hence
v + u in A
; :: thesis: verumper cases
( u = v or v <> u )
;

end;

suppose
u = v
; :: thesis: v + u in A

then v + u =
((1. GF) * v) + v
by VECTSP_1:def 17

.= ((1. GF) * v) + ((1. GF) * v) by VECTSP_1:def 17

.= ((1. GF) + (1. GF)) * v by VECTSP_1:def 15 ;

hence v + u in A by A56, A66; :: thesis: verum

end;.= ((1. GF) * v) + ((1. GF) * v) by VECTSP_1:def 17

.= ((1. GF) + (1. GF)) * v by VECTSP_1:def 15 ;

hence v + u in A by A56, A66; :: thesis: verum

suppose A68:
v <> u
; :: thesis: v + u in A

deffunc H_{1}( set ) -> Element of the carrier of GF = 0. GF;

consider f being Function of V,GF such that

A69: ( f . v = 1. GF & f . u = 1. GF ) and

A70: for w being Element of V st w <> v & w <> u holds

f . w = H_{1}(w)
from FUNCT_2:sch 7(A68);

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

A71: Carrier f = {v,u}

A73: ( (1. GF) * u = u & (1. GF) * v = v ) by VECTSP_1:def 17;

reconsider f = f as Linear_Combination of A by A72, Def4;

consider F being FinSequence of V such that

A74: ( F is one-to-one & rng F = Carrier f ) and

A75: Sum (f (#) F) = Sum f by Def6;

( F = <*v,u*> or F = <*u,v*> ) by A68, A71, A74, FINSEQ_3:99;

then ( f (#) F = <*((1. GF) * v),((1. GF) * u)*> or f (#) F = <*((1. GF) * u),((1. GF) * v)*> ) by A69, Th11;

then Sum f = v + u by A75, A73, RLVECT_1:45;

hence v + u in A by A54; :: thesis: verum

end;consider f being Function of V,GF such that

A69: ( f . v = 1. GF & f . u = 1. GF ) and

A70: for w being Element of V st w <> v & w <> u holds

f . w = H

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

now :: thesis: for w being Element of V st not w in {v,u} holds

f . w = 0. GF

then reconsider f = f as Linear_Combination of V by Def1;f . w = 0. GF

let w be Element of V; :: thesis: ( not w in {v,u} implies f . w = 0. GF )

assume not w in {v,u} ; :: thesis: f . w = 0. GF

then ( w <> v & w <> u ) by TARSKI:def 2;

hence f . w = 0. GF by A70; :: thesis: verum

end;assume not w in {v,u} ; :: thesis: f . w = 0. GF

then ( w <> v & w <> u ) by TARSKI:def 2;

hence f . w = 0. GF by A70; :: thesis: verum

A71: Carrier f = {v,u}

proof

then A72:
Carrier f c= A
by A66, A67, ZFMISC_1:32;
thus
Carrier f c= {v,u}
:: according to XBOOLE_0:def 10 :: thesis: {v,u} c= Carrier f

assume x in {v,u} ; :: thesis: x in Carrier f

then ( x = v or x = u ) by TARSKI:def 2;

hence x in Carrier f by A1, A69; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v,u} or x in Carrier f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v,u} )

assume x in Carrier f ; :: thesis: x in {v,u}

then ex w being Element of V st

( x = w & f . w <> 0. GF ) ;

then ( x = v or x = u ) by A70;

hence x in {v,u} by TARSKI:def 2; :: thesis: verum

end;assume x in Carrier f ; :: thesis: x in {v,u}

then ex w being Element of V st

( x = w & f . w <> 0. GF ) ;

then ( x = v or x = u ) by A70;

hence x in {v,u} by TARSKI:def 2; :: thesis: verum

assume x in {v,u} ; :: thesis: x in Carrier f

then ( x = v or x = u ) by TARSKI:def 2;

hence x in Carrier f by A1, A69; :: thesis: verum

A73: ( (1. GF) * u = u & (1. GF) * v = v ) by VECTSP_1:def 17;

reconsider f = f as Linear_Combination of A by A72, Def4;

consider F being FinSequence of V such that

A74: ( F is one-to-one & rng F = Carrier f ) and

A75: Sum (f (#) F) = Sum f by Def6;

( F = <*v,u*> or F = <*u,v*> ) by A68, A71, A74, FINSEQ_3:99;

then ( f (#) F = <*((1. GF) * v),((1. GF) * u)*> or f (#) F = <*((1. GF) * u),((1. GF) * v)*> ) by A69, Th11;

then Sum f = v + u by A75, A73, RLVECT_1:45;

hence v + u in A by A54; :: thesis: verum

for b

( not b