Copyright (c) 1990 Association of Mizar Users
environ vocabulary FUNCT_1, FINSEQ_1, RLVECT_1, RELAT_1, FINSEQ_4, ARYTM_1, FUNCT_2, BOOLE, FINSET_1, SEQ_1, RLSUB_1, CARD_1, QC_LANG1, BINOP_1, RLVECT_2; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, REAL_1, RLSUB_1, FRAENKEL, NAT_1, BINOP_1, FINSEQ_4, CARD_1, PRE_TOPC; constructors REAL_1, RLSUB_1, DOMAIN_1, FRAENKEL, NAT_1, BINOP_1, FINSEQ_4, PRE_TOPC, XREAL_0, MEMBERED, XBOOLE_0; clusters RLVECT_1, RLSUB_1, RELSET_1, STRUCT_0, FINSET_1, PRE_TOPC, ARYTM_3, FUNCT_2, MEMBERED, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions FUNCT_1, RLSUB_1, STRUCT_0, TARSKI, XBOOLE_0; theorems BINOP_1, CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2, NAT_1, REAL_1, RLSUB_1, RLSUB_2, RLVECT_1, SUBSET_1, TARSKI, ZFMISC_1, AXIOMS, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, INT_1, XCMPLX_0, XCMPLX_1; schemes BINOP_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0; begin scheme LambdaSep1{D, R() -> non empty set, A() -> Element of D(), B() -> Element of R(), F(set) -> Element of R()}: ex f being Function of D(),R() st f.A() = B() & for x being Element of D() st x <> A() holds f.x = F(x) proof defpred P[set,set] means ($1 = A() implies $2 = B()) & ($1 <> A() implies $2 = F($1)); A1: for x being Element of D() ex y being Element of R() st P[x,y] proof let x be Element of D(); (x = A() implies thesis) & (x <> A() implies thesis); hence thesis; end; consider f being Function of D(),R() such that A2: for x being Element of D() holds P[x,f.x] from FuncExD(A1); take f; thus thesis by A2; end; scheme LambdaSep2{D, R() -> non empty set, A1, A2() -> Element of D(), B1, B2() -> Element of R(), F(set) -> Element of R()}: ex f being Function of D(),R() st f.A1() = B1() & f.A2() = B2() & for x being Element of D() st x <> A1() & x <> A2() holds f.x = F(x) provided A1: A1() <> A2() proof defpred P[set,set] means ($1 = A1() implies $2 = B1()) & ($1 = A2() implies $2 = B2()) & ($1 <> A1() & $1 <> A2() implies $2 = F($1)); A2: for x being Element of D() ex y being Element of R() st P[x,y] proof let x be Element of D(); (x = A1() implies thesis) & (x = A2() implies thesis) & (x <> A1() & x <> A2() implies thesis) by A1; hence thesis; end; consider f being Function of D(),R() such that A3: for x being Element of D() holds P[x,f.x] from FuncExD(A2); take f; thus thesis by A3; end; reserve X,Y,x,y,y1,y2 for set, p for FinSequence, i,j,k,l,n for Nat, V for RealLinearSpace, u,v,v1,v2,v3,w for VECTOR of V, a,b for Real, F,G,H1,H2 for FinSequence of the carrier of V, A,B for Subset of V, f for Function of the carrier of V, REAL; definition let S be 1-sorted; let x; assume A1: x in S; func vector(S,x) -> Element of S equals :Def1: x; coherence by A1,RLVECT_1:def 1; end; canceled 2; theorem Th3: for S being non empty 1-sorted,v being Element of S holds vector(S,v) = v proof let S be non empty 1-sorted,v be Element of S; v in S by RLVECT_1:3; hence thesis by Def1; end; theorem Th4: for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G,H being FinSequence of the carrier of V st len F = len G & len F = len H & for k st k in dom F holds H.k = F/.k + G/.k holds Sum(H) = Sum(F) + Sum(G) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr); defpred P[Nat] means for F,G,H be FinSequence of the carrier of V st len F = $1 & len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k + G/.k) holds Sum(H) = Sum(F) + Sum(G); A1: P[0] proof let F,G,H be FinSequence of the carrier of V; assume len F = 0 & len F = len G & len F = len H; then Sum(F) = 0.V & Sum(G) = 0.V & Sum(H) = 0.V & 0.V + 0.V = 0.V by RLVECT_1:10,94; hence thesis; end; A2: for k st P[k] holds P[k+1] proof now let k; assume A3: for F,G,H be FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k + G/.k) holds Sum(H) = Sum(F) + Sum(G); let F,G,H be FinSequence of the carrier of V; assume that A4: len F = k + 1 and A5: len F = len G and A6: len F = len H and A7: for k st k in dom F holds H.k = F/.k + G/.k; reconsider f = F | Seg k,g = G | Seg k,h = H | Seg k as FinSequence of the carrier of V by FINSEQ_1:23; A8: len f = k & len g = k & len h = k by A4,A5,A6,FINSEQ_3:59; now let i; assume A9: i in dom f; then A10: i in dom g & i in dom h by A8,FINSEQ_3:31; then A11: F.i = f.i & G.i = g.i & H.i = h.i by A9,FUNCT_1:70; len f <= len F by A4,A8,NAT_1:37; then A12: dom f c= dom F by FINSEQ_3:32; then i in dom F by A9; then i in dom F & i in dom G by A5,FINSEQ_3:31; then F/.i = F.i & G/.i = G.i by FINSEQ_4:def 4; then f/.i = F/.i & g/.i = G/.i by A9,A10,A11,FINSEQ_4:def 4; hence h.i = f/.i + g/.i by A7,A9,A11,A12; end; then A13: Sum(h) = Sum(f) + Sum(g) by A3,A8; k + 1 in Seg(k + 1) by FINSEQ_1:6; then A14: k + 1 in dom F & k + 1 in dom G & k + 1 in dom H by A4,A5,A6,FINSEQ_1:def 3; then F.(k + 1) in rng F & G.(k + 1) in rng G & H.(k + 1) in rng H & rng F c= the carrier of V & rng G c= the carrier of V & rng H c= the carrier of V by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider v = F.(k + 1),u = G.(k + 1),w = H.(k + 1) as Element of V; A15: G = g ^ <* u *> & F = f ^ <* v *> & H = h ^ <* w *> by A4,A5,A6,FINSEQ_3:61; then A16: Sum(G) = Sum(g) + Sum<* u *> & Sum(F) = Sum(f) + Sum<* v *> & Sum<* v *> = v & Sum<* u *> = u by RLVECT_1:58,61; A17: w = F/.(k + 1) + G/.(k + 1) by A7,A14 .= v + G/.(k + 1) by A14,FINSEQ_4:def 4 .= v + u by A14,FINSEQ_4:def 4; thus Sum(H) = Sum(h) + Sum<* w *> by A15,RLVECT_1:58 .= Sum(f) + Sum(g) + (v + u) by A13,A17,RLVECT_1:61 .= Sum(f) + Sum(g) + v + u by RLVECT_1:def 6 .= Sum(F) + Sum(g) + u by A16,RLVECT_1:def 6 .= Sum(F) + Sum(G) by A16,RLVECT_1:def 6; end; hence thesis; end; for k holds P[k] from Ind(A1,A2); hence thesis; end; theorem len F = len G & (for k st k in dom F holds G.k = a * F/.k) implies Sum(G) = a * Sum(F) proof assume that A1: len F = len G and A2: for k st k in dom F holds G.k = a * F/.k; A3: dom F = Seg len F & dom G = Seg len G by FINSEQ_1:def 3; now let k,v; assume that A4: k in dom G and A5: v = F.k; v = F/.k by A1,A3,A4,A5,FINSEQ_4:def 4; hence G.k = a * v by A1,A2,A3,A4; end; hence thesis by A1,RLVECT_1:56; end; theorem Th6: for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G being FinSequence of the carrier of V st len F = len G & (for k st k in dom F holds G.k = - F/.k) holds Sum(G) = - Sum(F) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G be FinSequence of the carrier of V; assume that A1: len F = len G and A2: for k st k in dom F holds G.k = - F/.k; now let k; let v be Element of V; assume that A3: k in dom G and A4: v = F.k; A5: dom G = Seg len G & dom F = Seg len F by FINSEQ_1:def 3; then v = F/.k by A1,A3,A4,FINSEQ_4:def 4; hence G.k = - v by A1,A2,A3,A5; end; hence thesis by A1,RLVECT_1:57; end; theorem for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G,H being FinSequence of the carrier of V st len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k - G/.k) holds Sum(H) = Sum(F) - Sum(G) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G,H be FinSequence of the carrier of V; assume that A1: len F = len G & len F = len H and A2: for k st k in dom F holds H.k = F/.k - G/.k; A3: dom G = Seg len G by FINSEQ_1:def 3; deffunc Q(set)= - G/.$1; consider I being FinSequence such that A4: len I = len G and A5: for k st k in Seg len G holds I.k = Q(k) from SeqLambda; rng I c= the carrier of V proof let x; assume x in rng I; then consider y such that A6: y in dom I & I.y = x by FUNCT_1:def 5; reconsider y as Nat by A6,FINSEQ_3:25; y in Seg(len G) by A4,A6,FINSEQ_1:def 3; then x = - G/.y by A5,A6; then reconsider v = x as Element of V; v in V by RLVECT_1:3; hence thesis; end; then reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4; A7: Sum(I) = - Sum(G) by A3,A4,A5,Th6; now let k; A8: dom F = Seg len F & dom I = Seg len I by FINSEQ_1:def 3; assume A9: k in dom F; then A10: I.k = I/.k by A1,A4,A8,FINSEQ_4:def 4; thus H.k = F/.k - G/.k by A2,A9 .= F/.k + (- G/.k) by RLVECT_1:def 11 .= F/.k + I/.k by A1,A5,A8,A9,A10; end; then Sum(H) = Sum(F) + Sum(I) by A1,A4,Th4; hence thesis by A7,RLVECT_1:def 11; end; Lm1: k < n implies n - 1 is Nat proof assume k < n; then k + 1 <= n by NAT_1:38; then consider j such that A1: n = k + 1 + j by NAT_1:28; n - 1 = k + (j + 1) - 1 by A1,XCMPLX_1:1 .= k + ((j + 1) - 1) by XCMPLX_1:29 .= k + j by XCMPLX_1:26; hence thesis; end; theorem Th8: for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G being FinSequence of the carrier of V for f being Permutation of dom F st len F = len G & (for i st i in dom G holds G.i = F.(f.i)) holds Sum(F) = Sum(G) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G be FinSequence of the carrier of V; let f be Permutation of dom F; defpred P[Nat] means for H1,H2 be FinSequence of the carrier of V st len H1 = $1 & len H1 = len H2 for f being Permutation of dom H1 st (for i st i in dom H2 holds H2.i = H1.(f.i)) holds Sum(H1) = Sum(H2); A1: P[0] proof let H1,H2 be FinSequence of the carrier of V; assume len H1 = 0 & len H1 = len H2; then Sum(H1) = 0.V & Sum(H2) = 0.V by RLVECT_1:94; hence thesis; end; A2: for k st P[k] holds P[k+1] proof now let k; assume A3: for H1,H2 be FinSequence of the carrier of V st len H1 = k & len H1 = len H2 for f being Permutation of dom H1 st (for i st i in dom H2 holds H2.i = H1.(f.i)) holds Sum(H1) = Sum(H2); let H1,H2 be FinSequence of the carrier of V; assume that A4: len H1 = k + 1 and A5: len H1 = len H2; let f be Permutation of dom H1; assume A6: for i st i in dom H2 holds H2.i = H1.(f.i); reconsider p = H2 | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:23; A7: k + 1 in Seg(k + 1) by FINSEQ_1:6; A8: dom H2 = Seg(k + 1) & dom H1 = Seg(k + 1) by A4,A5,FINSEQ_1:def 3; Seg(k + 1) = {} implies Seg(k + 1) = {}; then A9: dom f = Seg(k + 1) & rng f = Seg(k + 1) by A8,FUNCT_2:def 1,def 3; then A10: f.(k + 1) in Seg(k + 1) by A7,FUNCT_1:def 5; then reconsider n = f.(k + 1) as Nat; A11: H2.(k + 1) = H1.(f.(k + 1)) by A6,A7,A8; reconsider v = H2.(k + 1) as Element of V by A4,A5,A7,RLVECT_1:54; 1 <= n by A10,FINSEQ_1:3; then consider m1 being Nat such that A12: 1 + m1 = n by NAT_1:28; A13: n <= k + 1 by A10,FINSEQ_1:3; then consider m2 being Nat such that A14: n + m2 = k + 1 by NAT_1:28; reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:23; defpred P[Nat,set] means $2 = H1.(n + $1); A15: for j,y1,y2 st j in Seg m2 & P[j,y1] & P[j,y2] holds y1 = y2; A16: for j st j in Seg m2 ex x st P[j,x]; consider q2 being FinSequence such that A17: dom q2 = Seg m2 and A18: for k st k in Seg m2 holds P[k,q2.k] from SeqEx(A15,A16); rng q2 c= the carrier of V proof let x; assume x in rng q2; then consider y such that A19: y in dom q2 and A20: x = q2.y by FUNCT_1:def 5; reconsider y as Nat by A17,A19; 1 <= y & y <= n + y by A17,A19,FINSEQ_1:3,NAT_1:37; then A21: 1 <= n + y by AXIOMS:22; y <= m2 by A17,A19,FINSEQ_1:3; then n + y <= len H1 by A4,A14,REAL_1:55; then n + y in Seg(len H1) by A21,FINSEQ_1:3; then reconsider xx = H1.(n + y) as Element of V by RLVECT_1:54; xx in the carrier of V; hence thesis by A17,A18,A19,A20; end; then reconsider q2 as FinSequence of the carrier of V by FINSEQ_1:def 4; set q = q1 ^ q2; A22: k <= k + 1 by NAT_1:37; then A23: len p = k by A4,A5,FINSEQ_1:21; m1 <= n by A12,NAT_1:29; then A24: m1 <= k + 1 by A13,AXIOMS:22; then A25: len q1 = m1 & len q2 = m2 by A4,A17,FINSEQ_1:21,def 3; then A26: len q = m1 + m2 by FINSEQ_1:35; A27: 1 + k = 1 + (m1 + m2) by A12,A14,XCMPLX_1:1; then A28: len q = k by A26,XCMPLX_1:2; len(q1 ^ <* v *>) + len q2 = len q1 + len<* v *> + m2 by A25,FINSEQ_1:35 .= k + 1 by A12,A14,A25,FINSEQ_1:57; then A29: dom H1 = Seg(len(q1 ^ <* v *>) + len q2) by A4,FINSEQ_1:def 3; A30: now let j; assume A31: j in dom(q1 ^ <* v *>); len(q1 ^ <* v *>) = m1 + len <* v *> by A25,FINSEQ_1:35 .= m1 + 1 by FINSEQ_1:57; then j in Seg(m1 + 1) by A31,FINSEQ_1:def 3; then A32: j in Seg m1 \/ {n} by A12,FINSEQ_1:11; A33: now assume j in Seg m1; then A34: j in dom q1 by A4,A24,FINSEQ_1:21; then q1.j = H1.j by FUNCT_1:70; hence H1.j = (q1 ^ <* v *>).j by A34,FINSEQ_1:def 7; end; now assume j in {n}; then A35: j = n by TARSKI:def 1; 1 in Seg 1 & len<* v *> = 1 by FINSEQ_1:3,56; then 1 in dom <* v *> by FINSEQ_1:def 3; then (q1 ^ <* v *>).(len q1 + 1) = <* v *>.1 by FINSEQ_1:def 7; hence (q1 ^ <* v *>).j = H1.j by A11,A12,A25,A35,FINSEQ_1:57; end; hence H1.j = (q1 ^ <* v *>).j by A32,A33,XBOOLE_0:def 2; end; now let j; assume A36: j in dom q2; len(q1 ^ <* v *>) = m1 + len<* v *> by A25,FINSEQ_1:35 .= n by A12,FINSEQ_1:56; hence H1.(len(q1 ^ <* v *>) + j) = q2.j by A17,A18,A36; end; then A37: H1 = q1 ^ <* v *> ^ q2 by A29,A30,FINSEQ_1:def 7; k = m1 + m2 by A27,XCMPLX_1:2; then A38: m1 <= k by NAT_1:29; A39: Seg k c= Seg(k + 1) by A22,FINSEQ_1:7; A40: now let n; assume n in dom f; then f.n in Seg(k + 1) by A9,FUNCT_1:def 5; hence f.n is Nat; end; A41: dom q1 = Seg m1 by A4,A24,FINSEQ_1:21; A42: dom p = Seg k & dom q = Seg k by A4,A5,A22,A28,FINSEQ_1:21,def 3; defpred P[set,set] means (f.$1 in dom q1 implies $2 = f.$1) & (not f.$1 in dom q1 implies for l st l = f.$1 holds $2 = l - 1); A43: for i st i in Seg k ex y st P[i,y] proof let i; assume A44: i in Seg k; now assume A45: not f.i in dom q1; f.i in Seg(k + 1) by A9,A39,A44,FUNCT_1:def 5; then reconsider j = f.i as Nat; take y = j - 1; thus f.i in dom q1 implies y = f.i by A45; assume not f.i in dom q1; let t be Nat; assume t = f.i; hence y = t - 1; end; hence thesis; end; A46: for i,y1,y2 st i in Seg k & P[i,y1] & P[i,y2] holds y1 = y2 proof let i,y1,y2; assume that A47: i in Seg k and A48: f.i in dom q1 implies y1 = f.i and A49: not f.i in dom q1 implies for l st l = f.i holds y1 = l - 1 and A50: f.i in dom q1 implies y2 = f.i and A51: not f.i in dom q1 implies for l st l = f.i holds y2 = l - 1; now assume A52: not f.i in dom q1; f.i in Seg(k + 1) by A9,A39,A47,FUNCT_1:def 5; then reconsider j = f.i as Nat; y1 = j - 1 & y2 = j - 1 by A49,A51,A52; hence thesis; end; hence y1 = y2 by A48,A50; end; consider g being FinSequence such that A53: dom g = Seg k and A54: for i st i in Seg k holds P[i,g.i] from SeqEx(A46,A43); A55: now let i,l; assume that A56: l = f.i and A57: not f.i in dom q1 and A58: i in dom g; A59: f.i in rng f by A9,A39,A53,A58,FUNCT_1:def 5; l < 1 or m1 < l by A41,A56,A57,FINSEQ_1:3; then A60: m1 + 1 <= l by A9,A56,A59,FINSEQ_1:3,NAT_1:38; now assume m1 + 1 = l; then k + 1 = i by A7,A9,A12,A39,A53,A56,A58,FUNCT_1:def 8; then k + 1 <= k + 0 by A53,A58,FINSEQ_1:3; hence contradiction by REAL_1:53; end; then m1 + 1 < l by A60,REAL_1:def 5; then m1 + 1 + 1 <= l by NAT_1:38; then m1 + (1 + 1) <= l by XCMPLX_1:1; hence m1 + 2 <= l; end; A61: rng g c= dom p proof let y; assume y in rng g; then consider x such that A62: x in dom g and A63: g.x = y by FUNCT_1:def 5; reconsider x as Nat by A53,A62; now per cases; suppose A64: f.x in dom q1; then A65: f.x = g.x by A53,A54,A62; dom q1 c= dom p by A38,A41,A42,FINSEQ_1:7; hence thesis by A63,A64,A65; suppose A66: not f.x in dom q1; reconsider j = f.x as Nat by A9,A39,A40,A53,A62; j < 1 or m1 < j by A41,A66,FINSEQ_1:3; then A67: (j = 0 or m1 < j) & f.x in Seg(k + 1) by A9,A39,A53,A62,FUNCT_1:def 5,RLVECT_1:98; then reconsider l = j - 1 as Nat by Lm1,FINSEQ_1:3; A68: g.x = j - 1 by A53,A54,A62,A66; m1 + 2 <= j by A55,A62,A66; then m1 + 2 - 1 <= l by REAL_1:49; then m1 + (1 + 1 - 1) <= l by XCMPLX_1:29; then m1 + 1 <= l & 1 <= m1 + 1 by NAT_1:37; then A69: 1 <= l by AXIOMS:22; j <= k + 1 by A67,FINSEQ_1:3; then l <= (k + 1) - 1 by REAL_1:49; then l <= k + (1 - 1) by XCMPLX_1:29; hence thesis by A42,A63,A68,A69,FINSEQ_1:3; end; hence thesis; end; dom p = {} implies dom p = {}; then reconsider g as Function of dom q, dom q by A42,A53,A61,FUNCT_2:def 1,RELSET_1:11; A70: rng g = dom q proof thus rng g c= dom q by A42,A61; let y; assume A71: y in dom q; then consider x such that A72: x in dom f and A73: f.x = y by A9,A39,A42,FUNCT_1:def 5; reconsider x as Nat by A9,A72; reconsider j = y as Nat by A42,A71; now per cases; suppose A74: x in dom g; now per cases; suppose f.x in dom q1; then g.x = f.x by A53,A54,A74; hence thesis by A73,A74,FUNCT_1:def 5; suppose A75: not f.x in dom q1; j <= k by A42,A71,FINSEQ_1:3; then 1 <= j + 1 & j + 1 <= k + 1 by NAT_1:37,REAL_1:55; then j + 1 in rng f by A9,FINSEQ_1:3; then consider x1 being set such that A76: x1 in dom f and A77: f.x1 = j + 1 by FUNCT_1:def 5; A78: now assume not x1 in dom g; then x1 in Seg(k + 1) \ Seg k by A9,A53,A76,XBOOLE_0:def 4; then x1 in {k + 1} by FINSEQ_3:16; then j + 1 = m1 +1 by A12,A77,TARSKI:def 1; then 1 <= j & j <= m1 by A42,A71,FINSEQ_1:3,XCMPLX_1:2; hence contradiction by A41,A73,A75,FINSEQ_1:3; end; j < 1 or m1 < j by A41,A73,A75,FINSEQ_1:3; then not j + 1 <= m1 by A42,A71,FINSEQ_1:3,NAT_1:38; then not f.x1 in dom q1 & x1 is Nat by A9,A41,A76,A77,FINSEQ_1:3; then g.x1 = j + 1 - 1 by A53,A54,A77,A78 .= y by XCMPLX_1:26; hence thesis by A78,FUNCT_1:def 5; end; hence thesis; suppose not x in dom g; then x in Seg(k + 1) \ Seg k by A9,A53,A72,XBOOLE_0:def 4; then x in {k + 1} by FINSEQ_3:16; then A79: x = k + 1 by TARSKI:def 1; j <= k by A42,A71,FINSEQ_1:3; then 1 <= j + 1 & j + 1 <= k + 1 by NAT_1:37,REAL_1:55; then j + 1 in rng f by A9,FINSEQ_1:3; then consider x1 being set such that A80: x1 in dom f and A81: f.x1 = j + 1 by FUNCT_1:def 5; A82: now assume not x1 in dom g; then x1 in Seg(k + 1) \ Seg k by A9,A53,A80,XBOOLE_0:def 4 ; then x1 in {k + 1} by FINSEQ_3:16; then j + 1 = j + 0 by A73,A79,A81,TARSKI:def 1; hence contradiction by XCMPLX_1:2; end; m1 <= j by A12,A73,A79,REAL_1:69; then not j + 1 <= m1 by NAT_1:38; then not f.x1 in dom q1 & x1 is Nat by A9,A41,A80,A81,FINSEQ_1:3; then g.x1 = j + 1 - 1 by A53,A54,A81,A82 .= y by XCMPLX_1:26; hence thesis by A82,FUNCT_1:def 5; end; hence y in rng g; end; g is one-to-one proof let y1,y2; assume that A83: y1 in dom g & y2 in dom g and A84: g.y1 = g.y2; reconsider j1 = y1, j2 = y2 as Nat by A53,A83; A85: f.y1 in Seg(k + 1) & f.y2 in Seg(k + 1) by A9,A39,A53,A83,FUNCT_1:def 5; then reconsider a = f.y1, b = f.y2 as Nat; now per cases; suppose f.y1 in dom q1 & f.y2 in dom q1; then g.j1 = f.y1 & g.j2 = f.y2 by A53,A54,A83; hence thesis by A9,A39,A53,A83,A84,FUNCT_1:def 8; suppose A86: f.y1 in dom q1 & not f.y2 in dom q1; then A87: g.j1 = a & g.j2 = b - 1 by A53,A54,A83; a <= m1 & 1 <= b by A41,A85,A86,FINSEQ_1:3; then (b - 1) + 1 <= m1 + 1 & 1 <= b by A84,A87,AXIOMS:24; then 1 <= b & b <= m1 + 1 by XCMPLX_1:27; then b in Seg(m1 + 1) & not b in Seg m1 by A4,A24,A86,FINSEQ_1:3,21; then b in Seg(m1 + 1) \ Seg m1 by XBOOLE_0:def 4; then b in {m1 + 1} by FINSEQ_3:16; then b = m1 + 1 by TARSKI:def 1; then y2 = k + 1 by A7,A9,A12,A39,A53,A83,FUNCT_1:def 8; hence thesis by A53,A83,FINSEQ_3:9; suppose A88: not f.y1 in dom q1 & f.y2 in dom q1; then A89: g.j1 = a - 1 & g.j2 = b by A53,A54,A83; b <= m1 & 1 <= a by A41,A85,A88,FINSEQ_1:3; then (a - 1) + 1 <= m1 + 1 & 1 <= a by A84,A89,AXIOMS:24; then 1 <= a & a <= m1 + 1 by XCMPLX_1:27; then a in Seg(m1 + 1) & not a in Seg m1 by A4,A24,A88,FINSEQ_1:3,21; then a in Seg(m1 + 1) \ Seg m1 by XBOOLE_0:def 4; then a in {m1 + 1} by FINSEQ_3:16; then a = m1 + 1 by TARSKI:def 1; then y1 = k + 1 by A7,A9,A12,A39,A53,A83,FUNCT_1:def 8; hence thesis by A53,A83,FINSEQ_3:9; suppose not f.y1 in dom q1 & not f.y2 in dom q1; then g.j1 = a - 1 & g.j2 = b - 1 by A53,A54,A83; then g.j1 = a + (- 1) & g.y2 = b + (- 1) by XCMPLX_0:def 8; then a = b by A84,XCMPLX_1:2; hence thesis by A9,A39,A53,A83,FUNCT_1:def 8; end; hence thesis; end; then reconsider g as Permutation of dom q by A70,FUNCT_2:83; now let i; assume A90: i in dom p; then f.i in rng f by A9,A39,A42,FUNCT_1:def 5; then reconsider j = f.i as Nat by A9; now per cases; suppose f.i in dom q1; then f.i = g.i & H2.i = p.i & H1.(j) = q1.(j) & H2.i = H1.(f.i) & q1.j = q.j by A6,A8,A39,A42,A54,A90,FINSEQ_1:def 7,FUNCT_1:70; hence p.i = q.(g.i); suppose A91: not f.i in dom q1; then A92: g.i = j - 1 & H2.i = p.i & H2.i = H1.(f.i) by A6,A8,A39,A42,A54,A90,FUNCT_1:70; then A93: j - 1 in dom q by A42,A53,A70,A90,FUNCT_1:def 5; m1 + 2 <= j by A42,A53,A55,A90,A91; then m1 + 2 - 1 <= j - 1 by REAL_1:49; then m1 + (1 + 1 - 1) <= j - 1 by XCMPLX_1:29; then m1 < m1 + 1 & m1 + 1 <= j - 1 by REAL_1:69; then A94: m1 < j - 1 & j - 1 < j by AXIOMS:22,INT_1:26; then m1 < j by AXIOMS:22; then reconsider j1 = j - 1 as Nat by Lm1; not j1 in dom q1 by A41,A94,FINSEQ_1:3; then consider a being Nat such that A95: a in dom q2 and A96: j1 = len q1 + a by A93,FINSEQ_1:38; A97: H1 = q1 ^ (<* v *> ^ q2) & j in dom H1 by A8,A9,A37,A39,A42,A90,FINSEQ_1:45,FUNCT_1:def 5; then consider b being Nat such that A98: b in dom(<* v *> ^ q2) and A99: j = len q1 + b by A91,FINSEQ_1:38; A100: q.(j - 1) = q2.a & H1.j = (<* v *> ^ q2).b by A95,A96,A97 ,A98,A99,FINSEQ_1:def 7; A101: len q1 = j1 - a by A96,XCMPLX_1:26; A102: b = j - len q1 by A99,XCMPLX_1:26 .= j - (j - 1) + a by A101,XCMPLX_1:37 .= j - j + 1 + a by XCMPLX_1:37 .= 0 + 1 + a by XCMPLX_1:14 .= 1 + a; len<* v *> = 1 by FINSEQ_1:56; hence p.i = q.(g.i) by A92,A95,A100,A102,FINSEQ_1:def 7; end; hence p.i = q.(g.i); end; then A103: Sum(p) = Sum(q) by A3,A23,A28; dom p = Seg len p & dom H1 = Seg len H1 & dom H2 = Seg len H2 by FINSEQ_1:def 3; then Sum(H2) = Sum(p) + v by A4,A5,A23,RLVECT_1:55 .= Sum(q) + Sum<* v *> by A103,RLVECT_1:61 .= Sum(q1) + Sum(q2) + Sum<* v *> by RLVECT_1:58 .= Sum(q1) + (Sum<* v *> + Sum(q2)) by RLVECT_1:def 6 .= Sum(q1) + Sum(<* v *> ^ q2) by RLVECT_1:58 .= Sum(q1 ^ (<* v *> ^ q2)) by RLVECT_1:58 .= Sum(H1) by A37,FINSEQ_1:45; hence Sum(H1) = Sum(H2); end; hence thesis; end; for k holds P[k] from Ind(A1,A2); hence thesis; end; theorem for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G being FinSequence of the carrier of V for f being Permutation of dom F st G = F * f holds Sum(F) = Sum(G) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G be FinSequence of the carrier of V; let f be Permutation of dom F; assume G = F * f; then len F = len G & for i st i in dom G holds G.i = F.(f.i) by FINSEQ_2:48,FUNCT_1:22; hence thesis by Th8; end; definition let V be 1-sorted; cluster empty finite Subset of V; existence proof {} is Subset of V by SUBSET_1:4; then {} is Subset of V & {} is finite; hence thesis; end; end; Lm2: X is finite & Y is finite implies X \+\ Y is finite proof assume X is finite & Y is finite; then X \ Y is finite & Y \ X is finite by FINSET_1:16; then (X \ Y) \/ (Y \ X) is finite by FINSET_1:14; hence thesis by XBOOLE_0:def 6; end; definition let V be 1-sorted; let S,T be finite Subset of V; redefine func S \/ T -> finite Subset of V; coherence proof S \/ T is finite; hence thesis; end; func S /\ T -> finite Subset of V; coherence proof S /\ T is finite; hence thesis; end; func S \ T -> finite Subset of V; coherence proof S \ T is finite; hence thesis; end; func S \+\ T -> finite Subset of V; coherence proof S \+\ T is finite by Lm2; hence thesis; end; end; definition let V be non empty LoopStr, T be finite Subset of V; assume A1:V is Abelian add-associative right_zeroed; canceled 2; func Sum(T) -> Element of V means :Def4: ex F be FinSequence of the carrier of V st rng F = T & F is one-to-one & it = Sum(F); existence proof consider p such that A2: rng p = T and A3: p is one-to-one by FINSEQ_4:73; reconsider p as FinSequence of the carrier of V by A2,FINSEQ_1:def 4; take Sum(p); take p; thus thesis by A2,A3; end; uniqueness by A1,RLVECT_1:59; end; definition let V be non empty 1-sorted; cluster non empty finite Subset of V; existence proof consider v being Element of V; {v} is finite Subset of V; hence thesis; end; end; definition let V be non empty 1-sorted; let v be Element of V; redefine func {v} -> finite Subset of V; coherence proof {v} is finite; hence thesis; end; end; definition let V be non empty 1-sorted; let v1,v2 be Element of V; redefine func {v1,v2} -> finite Subset of V; coherence proof {v1,v2} = {v1} \/ {v2} & {v1} is finite & {v2} is finite by ENUMSET1:41; hence thesis; end; end; definition let V be non empty 1-sorted; let v1,v2,v3 be Element of V; redefine func {v1,v2,v3} -> finite Subset of V; coherence proof {v1,v2,v3} = {v1} \/ {v2,v3} & {v1} is finite & {v2,v3} is finite by ENUMSET1:42; hence thesis; end; end; canceled 4; theorem Th14: for V be Abelian add-associative right_zeroed (non empty LoopStr) holds Sum({}V) = 0.V proof let V be Abelian add-associative right_zeroed (non empty LoopStr); A1: rng(<*>(the carrier of V)) = {}V by FINSEQ_1:27; Sum(<*>(the carrier of V)) = 0.V by RLVECT_1:60; hence thesis by A1,Def4,FINSEQ_3:101; end; theorem for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v be Element of V holds Sum{v} = v proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v be Element of V; rng<* v *> = {v} & <* v *> is one-to-one & Sum<* v *> = v by FINSEQ_1:56,FINSEQ_3:102,RLVECT_1:61; hence thesis by Def4; end; theorem for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v1,v2 be Element of V holds v1 <> v2 implies Sum{v1,v2} = v1 + v2 proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v1,v2 be Element of V; assume v1 <> v2; then rng<* v1,v2 *> = {v1,v2} & <* v1,v2 *> is one-to-one & Sum<* v1,v2 *> = v1 + v2 by FINSEQ_2:147,FINSEQ_3:103,RLVECT_1:62; hence thesis by Def4; end; theorem for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v1,v2,v3 be Element of V holds v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3 proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v1,v2,v3 be Element of V; assume v1 <> v2 & v2 <> v3 & v1 <> v3; then rng<* v1,v2,v3 *> = {v1,v2,v3} & <* v1,v2,v3 *> is one-to-one & Sum<* v1,v2,v3 *> = v1 + v2 + v3 by FINSEQ_2:148,FINSEQ_3:104,RLVECT_1:63; hence thesis by Def4; end; theorem Th18: for V be Abelian add-associative right_zeroed (non empty LoopStr), S,T be finite Subset of V holds T misses S implies Sum(T \/ S) = Sum(T) + Sum(S) proof let V be Abelian add-associative right_zeroed (non empty LoopStr), S,T be finite Subset of V; assume A1: T misses S; consider F be FinSequence of the carrier of V such that A2: rng F = T \/ S and A3: F is one-to-one & Sum(T \/ S) = Sum(F) by Def4; consider G be FinSequence of the carrier of V such that A4: rng G = T & G is one-to-one and A5: Sum(T) = Sum(G) by Def4; consider H be FinSequence of the carrier of V such that A6: rng H = S & H is one-to-one and A7: Sum(S) = Sum(H) by Def4; set I = G ^ H; A8: rng I = rng F by A2,A4,A6,FINSEQ_1:44; I is one-to-one by A1,A4,A6,FINSEQ_3:98; hence Sum(T \/ S) = Sum(I) by A3,A8,RLVECT_1:59 .= Sum(T) + Sum(S) by A5,A7,RLVECT_1:58; end; theorem Th19: for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V holds Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V; set A = S \ T; set B = T \ S; set Z = A \/ B; set I = T /\ S; Z = T \+\ S by XBOOLE_0:def 6; then A1: Z misses I & Z \/ I = T \/ S by XBOOLE_1:93,103; A2: A misses B by XBOOLE_1:82; A3: A misses I & A \/ I = S by XBOOLE_1:51,89; A4: B misses I & B \/ I = T by XBOOLE_1:51,89; Sum(T \/ S) + Sum(I) = Sum(Z) + Sum(I) + Sum(I) by A1,Th18 .= Sum(A) + Sum(B) + Sum(I) + Sum(I) by A2,Th18 .= Sum(A) + (Sum(I) + Sum(B)) + Sum(I) by RLVECT_1:def 6 .= (Sum(A) + Sum(I)) + (Sum(B) + Sum(I)) by RLVECT_1:def 6 .= Sum(S) + (Sum(B) + Sum(I)) by A3,Th18 .= Sum(T) + Sum(S) by A4,Th18; hence thesis by RLSUB_2:78; end; theorem for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V holds Sum(T /\ S) = Sum(T) + Sum(S) - Sum(T \/ S) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V; Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S) by Th19; then Sum(T) + Sum(S) = Sum(T /\ S) + Sum(T \/ S) by RLSUB_2:78; hence thesis by RLSUB_2:78; end; theorem Th21: for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V holds Sum(T \ S) = Sum(T \/ S) - Sum(S) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V; (T \ S) \/ S = T \/ S by XBOOLE_1:39; then A1: Sum(T \/ S) = Sum(T \ S) + Sum(S) - Sum((T \ S) /\ S) by Th19; (T \ S) misses S by XBOOLE_1:79; then (T \ S) /\ S = {}V by XBOOLE_0:def 7; then Sum(T \/ S) = Sum(T \ S) + Sum(S) - 0.V by A1,Th14 .= Sum(T \ S) + Sum(S) by RLVECT_1:26; hence thesis by RLSUB_2:78; end; theorem Th22: for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V holds Sum(T \ S) = Sum(T) - Sum(T /\ S) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V; T \ (T /\ S) = T \ S by XBOOLE_1:47; then Sum(T \ S) = Sum(T \/ (T /\ S)) - Sum(T /\ S) by Th21; hence thesis by XBOOLE_1:22; end; theorem for V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V holds Sum(T \+\ S) = Sum(T \/ S) - Sum(T /\ S) proof let V be Abelian add-associative right_zeroed right_complementable (non empty LoopStr), S,T be finite Subset of V; T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101; hence Sum(T \+\ S) = Sum(T \/ S) - Sum((T \/ S) /\ (T /\ S)) by Th22 .= Sum(T \/ S) - Sum((T \/ S) /\ T /\ S) by XBOOLE_1:16 .= Sum(T \/ S) - Sum(T /\ S) by XBOOLE_1:21; end; theorem for V be Abelian add-associative right_zeroed (non empty LoopStr), S,T be finite Subset of V holds Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T) proof let V be Abelian add-associative right_zeroed (non empty LoopStr), S,T be finite Subset of V; A1: T \ S misses S \ T by XBOOLE_1:82; thus Sum(T \+\ S) = Sum((T \ S) \/ (S \ T)) by XBOOLE_0:def 6 .= Sum(T \ S) + Sum(S \ T) by A1,Th18; end; definition let V be non empty ZeroStr; mode Linear_Combination of V -> Element of Funcs(the carrier of V, REAL) means :Def5: ex T being finite Subset of V st for v being Element of V st not v in T holds it.v = 0; existence proof deffunc F(Element of V)=0; consider f being Function of the carrier of V, REAL such that A1: for x being Element of V holds f.x = F(x) from LambdaD; reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:11; take f; {}V = {}; then reconsider P = {} as finite Subset of V; take P; thus thesis by A1; end; end; reserve K,L,L1,L2,L3 for Linear_Combination of V; definition let V be non empty LoopStr, L be Linear_Combination of V; func Carrier(L) -> finite Subset of V equals :Def6: {v where v is Element of V : L.v <> 0}; coherence proof set A = {v where v is Element of V : L.v <> 0}; consider T being finite Subset of V such that A1: for v being Element of V st not v in T holds L.v = 0 by Def5; A c= T proof let x; assume x in A; then ex v being Element of V st x = v & L.v <> 0; hence thesis by A1; end; then A is Subset of V & A is finite by FINSET_1:13,XBOOLE_1:1 ; hence A is finite Subset of V; end; end; canceled 3; theorem Th28: for V be non empty LoopStr, L be Linear_Combination of V, v be Element of V holds L.v = 0 iff not v in Carrier(L) proof let V be non empty LoopStr, L be Linear_Combination of V, v be Element of V; thus L.v = 0 implies not v in Carrier(L) proof assume A1: L.v = 0; assume not thesis; then v in {u where u is Element of V : L.u <> 0} by Def6; then ex u be Element of V st u = v & L.u <> 0; hence thesis by A1; end; assume not v in Carrier(L); then not v in {u where u is Element of V : L.u <> 0} by Def6; hence thesis; end; definition let V be non empty LoopStr; func ZeroLC(V) -> Linear_Combination of V means :Def7: Carrier (it) = {}; existence proof deffunc F(Element of V)=0; consider f being Function of the carrier of V, REAL such that A1: for x being Element of V holds f.x = F(x) from LambdaD; reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:11; f is Linear_Combination of V proof reconsider T = {}V as empty finite Subset of V; take T; thus thesis by A1; end; then reconsider f as Linear_Combination of V; take f; set C = {v where v is Element of V : f.v <> 0}; now assume A2: C <> {}; consider x being Element of C; x in C by A2; then ex v being Element of V st x = v & f.v <> 0; hence contradiction by A1; end; hence thesis by Def6; end; uniqueness proof let L,L' be Linear_Combination of V; assume that A3: Carrier(L) = {} and A4: Carrier(L') = {}; now let x; assume x in the carrier of V; then reconsider v = x as Element of V; A5: now assume L.v <> 0; then v in {u where u is Element of V : L.u <> 0}; hence contradiction by A3,Def6; end; now assume L'.v <> 0; then v in {u where u is Element of V : L'.u <> 0}; hence contradiction by A4,Def6; end; hence L.x = L'.x by A5; end; hence L = L' by FUNCT_2:18; end; end; canceled; theorem Th30: for V be non empty LoopStr, v be Element of V holds ZeroLC(V).v = 0 proof let V be non empty LoopStr, v be Element of V; Carrier (ZeroLC(V)) = {} & not v in {} by Def7; hence thesis by Th28; end; definition let V be non empty LoopStr; let A be Subset of V; mode Linear_Combination of A -> Linear_Combination of V means :Def8: Carrier (it) c= A; existence proof take L = ZeroLC(V); Carrier (L) = {} by Def7; hence thesis by XBOOLE_1:2; end; end; reserve l,l1,l2 for Linear_Combination of A; canceled 2; theorem A c= B implies l is Linear_Combination of B proof assume A1: A c= B; Carrier(l) c= A by Def8; then Carrier(l) c= B by A1,XBOOLE_1:1; hence thesis by Def8; end; theorem Th34: ZeroLC(V) is Linear_Combination of A proof Carrier(ZeroLC(V)) = {} & {} c= A by Def7,XBOOLE_1:2; hence thesis by Def8; end; theorem Th35: for l being Linear_Combination of {}the carrier of V holds l = ZeroLC(V) proof let l be Linear_Combination of {}(the carrier of V); Carrier(l) c= {} by Def8; then Carrier(l) = {} by XBOOLE_1:3; hence thesis by Def7; end; Lm3: for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds X = Y proof let f be Function; assume that A1: f " X = f " Y and A2: X c= rng f & Y c= rng f; X c= Y & Y c= X by A1,A2,FUNCT_1:158; hence thesis by XBOOLE_0:def 10; end; definition let V; let F; let f; func f (#) F -> FinSequence of the carrier of V means :Def9: len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i; existence proof deffunc Q(set)= f.(F/.$1) * F/.$1; consider G being FinSequence such that A1: len G = len F and A2: for n st n in Seg(len F) holds G.n = Q(n) from SeqLambda; rng G c= the carrier of V proof let x; assume x in rng G; then consider y such that A3: y in dom G and A4: G.y = x by FUNCT_1:def 5; A5: y in Seg(len F) by A1,A3,FINSEQ_1:def 3; then reconsider y as Nat; G.y = f.(F/.y) * F/.y & f.(F/.y) * F/.y in the carrier of V by A2,A5; hence thesis by A4; end; then reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4; take G; dom G = Seg(len F) by A1,FINSEQ_1:def 3; hence thesis by A1,A2; end; uniqueness proof let H1,H2; assume that A6: len H1 = len F and A7: for i st i in dom H1 holds H1.i = f.(F/.i) * F/.i and A8: len H2 = len F and A9: for i st i in dom H2 holds H2.i = f.(F/.i) * F/.i; now let k; assume 1 <= k & k <= len H1; then k in Seg(len H1) by FINSEQ_1:3; then k in dom H1 & k in dom H2 by A6,A8,FINSEQ_1:def 3; then H1.k = f.(F/.k) * F/.k & H2.k = f.(F/.k) * F/.k by A7,A9; hence H1.k = H2.k; end; hence thesis by A6,A8,FINSEQ_1:18; end; end; canceled 4; theorem Th40: i in dom F & v = F.i implies (f (#) F).i = f.v * v proof assume that A1: i in dom F and A2: v = F.i; len(f (#) F) = len F by Def9; then A3: i in dom(f (#) F) by A1,FINSEQ_3:31; F/.i = F.i by A1,FINSEQ_4:def 4; hence (f (#) F).i = f.v * v by A2,A3,Def9; end; theorem f (#) <*>(the carrier of V) = <*>(the carrier of V) proof len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def9 .= 0 by FINSEQ_1:32; hence thesis by FINSEQ_1:32; end; theorem Th42: f (#) <* v *> = <* f.v * v *> proof A1: len(f (#) <* v *>) = len<* v *> by Def9 .= 1 by FINSEQ_1:57; then dom(f (#) <* v *>) = {1} & 1 in {1} by FINSEQ_1:4,def 3,TARSKI:def 1; then (f (#) <* v *>).1 = f.(<* v *>/.1) * <* v *>/.1 by Def9 .= f.(<* v *>/.1) * v by FINSEQ_4:25 .= f.v * v by FINSEQ_4:25; hence thesis by A1,FINSEQ_1:57; end; theorem Th43: f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *> proof A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def9 .= 2 by FINSEQ_1:61; then A2: dom(f (#) <* v1,v2 *>) = {1,2} & 1 in {1,2} & 2 in {1,2} by FINSEQ_1:4,def 3,TARSKI:def 2; then A3: (f (#) <* v1,v2 *>).1 = f.(<* v1,v2 *>/.1) * <* v1,v2 *>/.1 by Def9 .= f.(<* v1,v2 *>/.1) * v1 by FINSEQ_4:26 .= f.v1 * v1 by FINSEQ_4:26; (f (#) <* v1,v2 *>).2 = f.(<* v1,v2 *>/.2) * <* v1,v2 *>/.2 by A2,Def9 .= f.(<* v1,v2 *>/.2) * v2 by FINSEQ_4:26 .= f.v2 * v2 by FINSEQ_4:26; hence thesis by A1,A3,FINSEQ_1:61; end; theorem f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *> proof A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def9 .= 3 by FINSEQ_1:62; then A2: dom(f (#) <* v1,v2,v3 *>) = {1,2,3} & 1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} by ENUMSET1:14,FINSEQ_1:def 3,FINSEQ_3:1; then A3: (f (#) <* v1,v2,v3 *>).1 = f.(<* v1,v2,v3 *>/.1) * <* v1,v2,v3 *>/.1 by Def9 .= f.(<* v1,v2,v3 *>/.1) * v1 by FINSEQ_4:27 .= f.v1 * v1 by FINSEQ_4:27; A4: (f (#) <* v1,v2,v3 *>).2 = f.(<* v1,v2,v3 *>/.2) * <* v1,v2,v3 *>/.2 by A2,Def9 .= f.(<* v1,v2,v3 *>/.2) * v2 by FINSEQ_4:27 .= f.v2 * v2 by FINSEQ_4:27; (f (#) <* v1,v2,v3 *>).3 = f.(<* v1,v2,v3 *>/.3) * <* v1,v2,v3 *>/.3 by A2,Def9 .= f.(<* v1,v2,v3 *>/.3) * v3 by FINSEQ_4:27 .= f.v3 * v3 by FINSEQ_4:27; hence thesis by A1,A3,A4,FINSEQ_1:62; end; definition let V; let L; func Sum(L) -> Element of V means :Def10: ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F); existence proof consider F being FinSequence such that A1: rng F = Carrier(L) and A2: F is one-to-one by FINSEQ_4:73; reconsider F as FinSequence of the carrier of V by A1,FINSEQ_1:def 4; take Sum(L (#) F); take F; thus F is one-to-one & rng F = Carrier(L) by A1,A2; thus thesis; end; uniqueness proof let v1,v2 be Element of V; given F1 being FinSequence of the carrier of V such that A3: F1 is one-to-one and A4: rng F1 = Carrier(L) and A5: v1 = Sum(L (#) F1); given F2 being FinSequence of the carrier of V such that A6: F2 is one-to-one and A7: rng F2 = Carrier(L) and A8: v2 = Sum(L (#) F2); set G1 = L (#) F1; set G2 = L (#) F2; A9: len F1 = len F2 & len G1 = len F1 & len G2 = len F2 by A3,A4,A6,A7,Def9,RLVECT_1:106; A10: dom F1 = Seg(len F1) & dom F2 = Seg(len F2) by FINSEQ_1:def 3; A11: dom(G1) = Seg(len G1) & dom G2 = Seg(len G2) by FINSEQ_1:def 3; defpred P[set,set] means {$2} = F1 " {F2.$1}; A12: for x st x in dom F1 ex y st y in dom F1 & P[x,y] proof let x; assume x in dom F1; then F2.x in rng F1 by A4,A7,A9,A10,FUNCT_1:def 5; then consider y such that A13: F1 " {F2.x} = {y} by A3,FUNCT_1:144; take y; y in F1 " {F2.x} by A13,TARSKI:def 1; hence y in dom F1 by FUNCT_1:def 13; thus thesis by A13; end; A14: dom F1 = {} implies dom F1 = {}; consider f being Function of dom F1, dom F1 such that A15: for x st x in dom F1 holds P[x,f.x] from FuncEx1(A12); A16: rng f = dom F1 proof thus rng f c= dom F1 by RELSET_1:12; let y; assume A17: y in dom F1; then F1.y in rng F2 by A4,A7,FUNCT_1:def 5; then consider x such that A18: x in dom F2 and A19: F2.x = F1.y by FUNCT_1:def 5; A20: x in dom f by A9,A10,A18,FUNCT_2:def 1; F1 " {F2.x} = F1 " (F1 .: {y}) by A17,A19,FUNCT_1:117; then F1 " {F2.x} c= {y} by A3,FUNCT_1:152; then {f.x} c= {y} by A9,A10,A15,A18; then f.x = y by ZFMISC_1:24; hence thesis by A20,FUNCT_1:def 5; end; f is one-to-one proof let y1,y2; assume that A21: y1 in dom f & y2 in dom f and A22: f.y1 = f.y2; A23: y1 in dom F1 & y2 in dom F1 by A14,A21,FUNCT_2:def 1; then A24: F1 " {F2.y1} = {f.y1} & F1 " {F2.y2} = {f.y2} by A15; F2.y1 in rng F1 & F2.y2 in rng F1 by A4,A7,A9,A10,A23,FUNCT_1:def 5 ; then {F2.y1} c= rng F1 & {F2.y2} c= rng F1 by ZFMISC_1:37; then {F2.y1} = {F2.y2} by A22,A24,Lm3; then F2.y1 = F2.y2 & y1 in dom F2 & y2 in dom F2 by A9,A10,A14,A21,FUNCT_2:def 1,ZFMISC_1:6; hence thesis by A6,FUNCT_1:def 8; end; then reconsider f as Permutation of dom F1 by A16,FUNCT_2:83; dom F1 = Seg(len F1) & dom G1 = Seg(len G1) by FINSEQ_1:def 3; then reconsider f as Permutation of dom G1 by A9; now let i; assume A25: i in dom G2; then reconsider u = F2.i as VECTOR of V by A9,A11,RLVECT_1:54; i in dom f by A9,A11,A25,FUNCT_2:def 1; then A26: f.i in dom F1 by A16,FUNCT_1:def 5; then reconsider m = f.i as Nat by A10; reconsider v = F1.m as VECTOR of V by A10,A26,RLVECT_1:54; {F1.(f.i)} = F1 .: {f.i} by A26,FUNCT_1:117 .= F1 .: (F1 " {F2.i}) by A9,A10,A11,A15,A25; then {F1.(f.i)} c= {F2.i} by FUNCT_1:145; then u = v & G2.i = L.(F2/.i) * F2/.i & G1.m = L.(F1/.m) * F1/.m & F1.m = F1/.m & F2.i = F2/.i by A9,A10,A11,A25,A26,Def9,FINSEQ_4:def 4,ZFMISC_1:24; hence G2.i = G1.(f.i); end; hence thesis by A5,A8,A9,Th8; end; end; Lm4: Sum(ZeroLC(V)) = 0.V proof consider F such that F is one-to-one and A1: rng F = Carrier(ZeroLC(V)) and A2: Sum(ZeroLC(V)) = Sum(ZeroLC(V) (#) F) by Def10; Carrier(ZeroLC(V)) = {} by Def7; then F = {} by A1,FINSEQ_1:27; then len F = 0 by FINSEQ_1:25; then len(ZeroLC(V) (#) F) = 0 by Def9; hence thesis by A2,RLVECT_1:94; end; canceled 2; theorem A <> {} & A is lineary-closed iff for l holds Sum(l) in A proof thus A <> {} & A is lineary-closed implies for l holds Sum(l) in A proof assume that A1: A <> {} and A2: A is lineary-closed; defpred P[Nat] means for l st card(Carrier(l)) = $1 holds Sum (l) in A; A3: P[0] proof now let l; assume card(Carrier(l)) = 0; then Carrier(l) = {} by CARD_2:59; then l = ZeroLC(V) by Def7; then Sum(l) = 0.V by Lm4; hence Sum(l) in A by A1,A2,RLSUB_1:4; end; hence thesis; end; A4: for k st P[k] holds P[k+1] proof now let k; assume A5: for l st card(Carrier(l)) = k holds Sum(l) in A; let l; assume A6: card(Carrier(l)) = k + 1; consider F such that A7: F is one-to-one and A8: rng F = Carrier(l) and A9: Sum(l) = Sum(l (#) F) by Def10; A10: len F = k + 1 by A6,A7,A8,FINSEQ_4:77; reconsider G = F | Seg k as FinSequence of the carrier of V by FINSEQ_1:23; A11: len G = k by A10,FINSEQ_3:59; A12: k + 1 in Seg(k + 1) by FINSEQ_1:6; then reconsider v = F.(k + 1) as VECTOR of V by A10,RLVECT_1:54; A13: k + 1 in dom F by A10,A12,FINSEQ_1:def 3; then A14: v in Carrier(l) & Carrier(l) c= A by A8,Def8,FUNCT_1:def 5 ; then A15: l.v * v in A by A2,RLSUB_1:def 1; deffunc F(Element of V)= l.$1; consider f being Function of the carrier of V, REAL such that A16: f.v = 0 and A17: for u being Element of V st u <> v holds f.u = F(u) from LambdaSep1; reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:11; now let u; assume A18: not u in Carrier(l); hence f.u = l.u by A14,A17 .= 0 by A18,Th28; end; then reconsider f as Linear_Combination of V by Def5; A19: Carrier(f) = Carrier(l) \ {v} proof thus Carrier(f) c= Carrier(l) \ {v} proof let x; assume x in Carrier(f); then x in {u : f.u <> 0} by Def6; then consider u such that A20: u = x & f.u <> 0; f.u = l.u by A16,A17,A20; then x in {w : l.w <> 0} & x <> v by A16,A20; then x in Carrier(l) & not x in {v} by Def6,TARSKI:def 1; hence thesis by XBOOLE_0:def 4; end; let x; assume A21: x in Carrier(l) \ {v}; then x in Carrier(l) by XBOOLE_0:def 4; then x in {u : l.u <> 0} by Def6; then consider u such that A22: x = u & l.u <> 0; not x in {v} by A21,XBOOLE_0:def 4; then x <> v by TARSKI:def 1; then l.u = f.u by A17,A22; then x in {w : f.w <> 0} by A22; hence thesis by Def6; end; then Carrier(f) c= A \ {v} & A \ {v} c= A by A14,XBOOLE_1:33,36; then Carrier(f) c= A by XBOOLE_1:1; then reconsider f as Linear_Combination of A by Def8; A23: G is one-to-one by A7,FUNCT_1:84; A24: rng G = Carrier(f) proof thus rng G c= Carrier(f) proof let x; assume x in rng G; then consider y such that A25: y in dom G and A26: G.y = x by FUNCT_1:def 5; reconsider y as Nat by A25,FINSEQ_3:25; dom G c= dom F by FUNCT_1:76; then A27: y in dom F & G.y = F.y by A25,FUNCT_1:70; then A28: x in rng F by A26,FUNCT_1:def 5; now assume x = v; then k + 1 = y & y <= k & k < k + 1 by A7,A11,A13,A25,A26,A27,FINSEQ_3:27,FUNCT_1:def 8,REAL_1:69; hence contradiction; end; then not x in {v} by TARSKI:def 1; hence thesis by A8,A19,A28,XBOOLE_0:def 4; end; let x; assume A29: x in Carrier(f); then x in rng F by A8,A19,XBOOLE_0:def 4; then consider y such that A30: y in dom F and A31: F.y = x by FUNCT_1:def 5; reconsider y as Nat by A30,FINSEQ_3:25; now assume not y in Seg k; then y in dom F \ Seg k by A30,XBOOLE_0:def 4; then y in Seg(k + 1) \ Seg k by A10,FINSEQ_1:def 3; then y in {k + 1} by FINSEQ_3:16; then y = k + 1 by TARSKI:def 1; then not v in {v} by A19,A29,A31,XBOOLE_0:def 4; hence contradiction by TARSKI:def 1; end; then y in dom F /\ Seg k by A30,XBOOLE_0:def 3; then A32: y in dom G by RELAT_1:90; then G.y = F.y by FUNCT_1:70; hence thesis by A31,A32,FUNCT_1:def 5; end; then A33: Sum(f (#) G) = Sum(f) by A23,Def10; A34: len(l (#) F) = k + 1 & len (f (#) G) = k by A10,A11,Def9; k <= k + 1 by NAT_1:37; then Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:9 .= dom(f (#) G) by A34,FINSEQ_1:def 3; then A35: dom(f (#) G) = dom(l (#) F) /\ Seg k by A34,FINSEQ_1:def 3; now let x; assume A36: x in dom(f (#) G); then reconsider n = x as Nat by FINSEQ_3:25; A37: n in dom G by A11,A34,A36,FINSEQ_3:31; then A38: G.n in rng G & rng G c= the carrier of V by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider u = G.n as VECTOR of V; not u in {v} by A19,A24,A38,XBOOLE_0:def 4; then A39: u <> v by TARSKI:def 1; A40: (f (#) G).n = f.u * u by A37,Th40 .= l.u * u by A17,A39; n in dom(l (#) F) by A35,A36,XBOOLE_0:def 3; then A41: n in dom F by A10,A34,FINSEQ_3:31; then F.n in rng F & rng F c= the carrier of V by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider w = F.n as VECTOR of V; w = u by A37,FUNCT_1:70; hence (f (#) G).x = (l (#) F).x by A40,A41,Th40; end; then A42: f (#) G = (l (#) F) | Seg k by A35,FUNCT_1:68; A43: dom(l (#) F) = Seg len (l (#) F) & dom(f (#) G) = Seg len (f (#) G) & dom F = Seg len F by FINSEQ_1:def 3; (l (#) F).(len F) = l.v * v by A10,A13,Th40; then A44: Sum(l (#) F) = Sum (f (#) G) + l.v * v by A10,A34,A42,A43,RLVECT_1:55; v in rng F by A13,FUNCT_1:def 5; then Carrier(l) is finite & {v} c= Carrier(l) by A8,ZFMISC_1:37; then card(Carrier(f)) = k + 1 - card{v} by A6,A19,CARD_2:63 .= k + 1 - 1 by CARD_1:79 .= k by XCMPLX_1:26; then Sum(f) in A by A5; hence Sum(l) in A by A2,A9,A15,A33,A44,RLSUB_1:def 1; end; hence thesis; end; A45: for k holds P[k] from Ind(A3,A4); let l; card(Carrier(l)) = card(Carrier(l)); hence Sum(l) in A by A45; end; assume A46: for l holds Sum(l) in A; ZeroLC(V) is Linear_Combination of A & Sum(ZeroLC(V)) = 0.V by Lm4,Th34; then A47: 0.V in A by A46; thus A <> {} by A46; A48: for a,v st v in A holds a * v in A proof let a,v; assume A49: v in A; now per cases; suppose a = 0; hence thesis by A47,RLVECT_1:23; suppose A50: a <> 0; deffunc F(Element of V) = 0; consider f such that A51: f.v = a and A52: for u being Element of V st u <> v holds f.u = F(u) from LambdaSep1; reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:11; now let u; assume not u in {v}; then u <> v by TARSKI:def 1; hence f.u = 0 by A52; end; then reconsider f as Linear_Combination of V by Def5; A53: Carrier(f) = {v} proof thus Carrier(f) c= {v} proof let x; assume x in Carrier(f); then x in {u : f.u <> 0} by Def6; then consider u such that A54: x = u & f.u <> 0; u = v by A52,A54; hence thesis by A54,TARSKI:def 1; end; let x; assume x in {v}; then x = v by TARSKI:def 1; then x in {u : f.u <> 0} by A50,A51; hence thesis by Def6; end; {v} c= A by A49,ZFMISC_1:37; then reconsider f as Linear_Combination of A by A53,Def8; consider F such that A55: F is one-to-one and A56: rng F = Carrier(f) and A57: Sum(f (#) F) = Sum(f) by Def10; F = <* v *> by A53,A55,A56,FINSEQ_3:106; then f (#) F = <* f.v * v *> by Th42; then Sum(f) = a * v by A51,A57,RLVECT_1:61; hence a * v in A by A46; end; hence thesis; end; thus for v,u st v in A & u in A holds v + u in A proof let v,u; assume that A58: v in A and A59: u in A; now per cases; suppose u = v; then v + u = 1 * v + v by RLVECT_1:def 9 .= 1 * v + 1 * v by RLVECT_1:def 9 .= (1 + 1) * v by RLVECT_1:def 9 .= 2 * v; hence thesis by A48,A58; suppose A60: v <> u; deffunc F(Element of V)=0; consider f such that A61: f.v = 1 and A62: f.u = 1 and A63: for w being Element of V st w <> v & w <> u holds f.w = F(w) from LambdaSep2(A60); reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:11; now let w; assume not w in {v,u}; then w <> v & w <> u by TARSKI:def 2; hence f.w = 0 by A63; end; then reconsider f as Linear_Combination of V by Def5; A64: Carrier(f) = {v,u} proof thus Carrier(f) c= {v,u} proof let x; assume x in Carrier(f); then x in {w : f.w <> 0} by Def6; then ex w st x = w & f.w <> 0; then x = v or x = u by A63; hence thesis by TARSKI:def 2; end; let x; assume x in {v,u}; then (x = v or x = u) & 0 <> 1 by TARSKI:def 2; then x in {w : f.w <> 0} by A61,A62; hence thesis by Def6; end; then Carrier(f) c= A by A58,A59,ZFMISC_1:38; then reconsider f as Linear_Combination of A by Def8; consider F such that A65: F is one-to-one and A66: rng F = Carrier(f) and A67: Sum(f (#) F) = Sum(f) by Def10; F = <* v,u *> or F = <* u,v *> by A60,A64,A65,A66,FINSEQ_3:108; then (f (#) F = <* 1 * v, 1 * u *> or f (#) F = <* 1 * u, 1* v *>) & 1 * u = u & 1 * v = v by A61,A62,Th43,RLVECT_1:def 9; then Sum(f) = v + u by A67,RLVECT_1:62; hence thesis by A46; end; hence thesis; end; thus thesis by A48; end; theorem Sum(ZeroLC(V)) = 0.V by Lm4; theorem for l being Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V proof let l be Linear_Combination of {}(the carrier of V); l = ZeroLC(V) by Th35; hence thesis by Lm4; end; theorem Th50: for l being Linear_Combination of {v} holds Sum(l) = l.v * v proof let l be Linear_Combination of {v}; A1: Carrier(l) c= {v} by Def8; now per cases by A1,ZFMISC_1:39; suppose Carrier(l) = {}; then A2: l = ZeroLC(V) by Def7; hence Sum(l) = 0.V by Lm4 .= 0 * v by RLVECT_1:23 .= l.v * v by A2,Th30; suppose Carrier(l) = {v}; then consider F such that A3: F is one-to-one & rng F = {v} and A4: Sum(l) = Sum(l (#) F) by Def10; F = <* v *> by A3,FINSEQ_3:106; then l (#) F = <* l.v * v *> by Th42; hence thesis by A4,RLVECT_1:61; end; hence thesis; end; theorem Th51: v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum(l) = l.v1 * v1 + l.v2 * v2 proof assume A1: v1 <> v2; let l be Linear_Combination of {v1,v2}; A2: Carrier(l) c= {v1,v2} by Def8; now per cases by A2,ZFMISC_1:42; suppose Carrier(l) = {}; then A3: l = ZeroLC(V) by Def7; hence Sum(l) = 0.V by Lm4 .= 0.V + 0.V by RLVECT_1:10 .= 0 * v1 + 0.V by RLVECT_1:23 .= 0 * v1 + 0 * v2 by RLVECT_1:23 .= l.v1 * v1 + 0 * v2 by A3,Th30 .= l.v1 * v1 + l.v2 * v2 by A3,Th30; suppose A4: Carrier(l) = {v1}; then reconsider L = l as Linear_Combination of {v1} by Def8; A5: not v2 in Carrier(l) by A1,A4,TARSKI:def 1; thus Sum(l) = Sum(L) .= l.v1 * v1 by Th50 .= l.v1 * v1 + 0.V by RLVECT_1:10 .= l.v1 * v1 + 0 * v2 by RLVECT_1:23 .= l.v1 * v1 + l.v2 * v2 by A5,Th28; suppose A6: Carrier(l) = {v2}; then reconsider L = l as Linear_Combination of {v2} by Def8; A7: not v1 in Carrier(l) by A1,A6,TARSKI:def 1; thus Sum(l) = Sum(L) .= l.v2 * v2 by Th50 .= 0.V + l.v2 * v2 by RLVECT_1:10 .= 0 * v1 + l.v2 * v2 by RLVECT_1:23 .= l.v1 * v1 + l.v2 * v2 by A7,Th28; suppose Carrier(l) = {v1,v2}; then consider F such that A8: F is one-to-one & rng F = {v1,v2} and A9: Sum(l) = Sum(l (#) F) by Def10; F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A8,FINSEQ_3:108; then l (#) F = <* l.v1 * v1, l.v2 * v2 *> or l (#) F = <* l.v2 * v2, l.v1 * v1 *> by Th43; hence Sum(l) = l.v1 * v1 + l.v2 * v2 by A9,RLVECT_1:62; end; hence thesis; end; theorem Carrier(L) = {} implies Sum(L) = 0.V proof assume Carrier(L) = {}; then L = ZeroLC(V) by Def7; hence thesis by Lm4; end; theorem Carrier(L) = {v} implies Sum(L) = L.v * v proof assume Carrier(L) = {v}; then L is Linear_Combination of {v} by Def8; hence thesis by Th50; end; theorem Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2 proof assume that A1: Carrier(L) = {v1,v2} and A2: v1 <> v2; L is Linear_Combination of {v1,v2} by A1,Def8; hence thesis by A2,Th51; end; definition let V be non empty LoopStr; let L1,L2 be Linear_Combination of V; redefine pred L1 = L2 means for v being Element of V holds L1.v = L2.v; compatibility by FUNCT_2:113; end; definition let V be non empty LoopStr; let L1,L2 be Linear_Combination of V; func L1 + L2 -> Linear_Combination of V means :Def12: for v being Element of V holds it.v = L1.v + L2.v; existence proof deffunc F(Element of V)=L1.$1 + L2.$1; consider f be Function of the carrier of V, REAL such that A1: for v being Element of V holds f.v = F(v) from LambdaD; reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:11; now let v be Element of V; assume not v in Carrier(L1) \/ Carrier(L2); then not v in Carrier(L1) & not v in Carrier(L2) by XBOOLE_0:def 2; then L1.v = 0 & L2.v = 0 by Th28; hence f.v = 0 + 0 by A1 .= 0; end; then reconsider f as Linear_Combination of V by Def5; take f; let v be Element of V; thus f.v = L1.v + L2.v by A1; thus thesis; end; uniqueness proof let M,N be Linear_Combination of V; assume A2: for v being Element of V holds M.v = L1.v + L2.v; assume A3: for v being Element of V holds N.v = L1.v + L2.v; let v be Element of V; thus M.v = L1.v + L2.v by A2 .= N.v by A3; end; end; canceled 3; theorem Th58: Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) proof let x; assume x in Carrier(L1 + L2); then x in {u : (L1 + L2).u <> 0} by Def6; then consider u such that A1: x = u and A2: (L1 + L2).u <> 0; (L1 + L2).u = L1.u + L2.u & 0 + 0 = 0 by Def12; then L1.u <> 0 or L2.u <> 0 by A2; then x in {v1 : L1.v1 <> 0} or x in {v2 : L2.v2 <> 0} by A1; then x in Carrier(L1) or x in Carrier(L2) by Def6; hence thesis by XBOOLE_0:def 2; end; theorem Th59: L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 + L2 is Linear_Combination of A proof assume L1 is Linear_Combination of A & L2 is Linear_Combination of A; then Carrier(L1) c= A & Carrier(L2) c= A by Def8; then Carrier(L1) \/ Carrier(L2) c= A & Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by Th58,XBOOLE_1:8; hence Carrier(L1 + L2) c= A by XBOOLE_1:1; end; theorem Th60: for V be non empty LoopStr, L1,L2 be Linear_Combination of V holds L1 + L2 = L2 + L1 proof let V be non empty LoopStr, L1,L2 be Linear_Combination of V; let v be Element of V; thus (L1 + L2).v = L2.v + L1.v by Def12 .= (L2 + L1).v by Def12; end; theorem Th61: L1 + (L2 + L3) = L1 + L2 + L3 proof let v; thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def12 .= L1.v + (L2.v + L3.v) by Def12 .= L1.v + L2.v + L3.v by XCMPLX_1:1 .= (L1 + L2).v + L3.v by Def12 .= (L1 + L2 + L3).v by Def12; end; theorem Th62: L + ZeroLC(V) = L & ZeroLC(V) + L = L proof thus L + ZeroLC(V) = L proof let v; thus (L + ZeroLC(V)).v = L.v + ZeroLC(V).v by Def12 .= L.v + 0 by Th30 .= L.v; end; hence thesis by Th60; end; definition let V,a; let L; func a * L -> Linear_Combination of V means :Def13: for v holds it.v = a * L.v; existence proof deffunc F(Element of V)=a * L.$1; consider f being Function of the carrier of V, REAL such that A1: for v being Element of V holds f.v = F(v) from LambdaD; reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:11; now let v; assume not v in Carrier(L); then L.v = 0 by Th28; hence f.v = a * 0 by A1 .= 0; end; then reconsider f as Linear_Combination of V by Def5; take f; let v; thus f.v = a * L.v by A1; thus thesis; end; uniqueness proof let L1,L2; assume A2: for v holds L1.v = a * L.v; assume A3: for v holds L2.v = a * L.v; let v; thus L1.v = a * L.v by A2 .= L2.v by A3; end; end; canceled 2; theorem Th65: a <> 0 implies Carrier(a * L) = Carrier(L) proof assume A1: a <> 0; set T = {u : (a * L).u <> 0}; set S = {v : L.v <> 0}; A2: T = S proof thus T c= S proof let x; assume x in T; then consider u such that A3: x = u and A4: (a * L).u <> 0; (a * L).u = a * L.u by Def13; then L.u <> 0 by A4; hence thesis by A3; end; let x; assume x in S; then consider v such that A5: x = v and A6: L.v <> 0; (a * L).v = a * L.v by Def13; then (a * L).v <> 0 by A1,A6,XCMPLX_1:6; hence thesis by A5; end; Carrier(a * L) = T & Carrier(L) = S by Def6; hence thesis by A2; end; theorem Th66: 0 * L = ZeroLC(V) proof let v; thus (0 * L).v = 0 * L.v by Def13 .= ZeroLC(V).v by Th30; end; theorem Th67: L is Linear_Combination of A implies a * L is Linear_Combination of A proof assume A1: L is Linear_Combination of A; now per cases; suppose a = 0; then a * L = ZeroLC(V) by Th66; hence thesis by Th34; suppose a <> 0; then Carrier(a * L) = Carrier(L) & Carrier(L) c= A by A1,Def8,Th65; hence thesis by Def8; end; hence thesis; end; theorem Th68: (a + b) * L = a * L + b * L proof let v; thus ((a + b) * L).v = (a + b) * L.v by Def13 .= a * L.v + b * L.v by XCMPLX_1:8 .= (a * L).v + b * L.v by Def13 .= (a * L).v + (b * L). v by Def13 .= ((a * L) + (b * L)).v by Def12; end; theorem Th69: a * (L1 + L2) = a * L1 + a * L2 proof let v; thus (a * (L1 + L2)).v = a * (L1 + L2).v by Def13 .= a * (L1.v + L2.v) by Def12 .= a * L1.v + a * L2.v by XCMPLX_1:8 .= (a * L1).v + a * L2.v by Def13 .= (a * L1).v + (a * L2). v by Def13 .= ((a * L1) + (a * L2)).v by Def12; end; theorem Th70: a * (b * L) = (a * b) * L proof let v; thus (a * (b * L)).v = a * (b * L).v by Def13 .= a * (b * L.v) by Def13 .= a * b * L.v by XCMPLX_1:4 .= ((a * b) * L).v by Def13; end; theorem Th71: 1 * L = L proof let v; thus (1 * L).v = 1 * L.v by Def13 .= L.v; end; definition let V,L; func - L -> Linear_Combination of V equals :Def14: (- 1) * L; correctness; end; canceled; theorem Th73: (- L).v = - L.v proof thus (- L).v = ((- 1) * L).v by Def14 .= (- 1) * L.v by Def13 .= - L.v by XCMPLX_1:180; end; theorem L1 + L2 = ZeroLC(V) implies L2 = - L1 proof assume A1: L1 + L2 = ZeroLC(V); let v; L1.v + L2.v = ZeroLC(V).v by A1,Def12 .= 0 by Th30; hence L2.v = - L1.v by XCMPLX_0:def 6 .= (- L1).v by Th73; end; theorem Th75: Carrier(- L) = Carrier(L) proof - 1 <> 0 & - L = (- 1) * L by Def14; hence thesis by Th65; end; theorem Th76: L is Linear_Combination of A implies - L is Linear_Combination of A proof - L = (- 1) * L by Def14; hence thesis by Th67; end; theorem - (- L) = L proof let v; thus (- (- L)).v = ((- 1) * (- L)).v by Def14 .= ((- 1) * ((- 1) * L)).v by Def14 .= ((- 1) * (- 1) * L).v by Th70 .= 1 * L.v by Def13 .= L.v; end; definition let V; let L1,L2; func L1 - L2 -> Linear_Combination of V equals :Def15: L1 + (- L2); correctness; end; canceled; theorem Th79: (L1 - L2).v = L1.v - L2.v proof thus (L1 - L2).v = (L1 + (- L2)).v by Def15 .= L1.v + (- L2).v by Def12 .= L1.v + (- L2.v) by Th73 .= L1.v - L2.v by XCMPLX_0:def 8; end; theorem Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2) proof L1 - L2 = L1 + (- L2) by Def15; then Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(- L2) by Th58; hence thesis by Th75; end; theorem L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 - L2 is Linear_Combination of A proof assume that A1: L1 is Linear_Combination of A and A2: L2 is Linear_Combination of A; A3: - L2 is Linear_Combination of A by A2,Th76; L1 - L2 = L1 + (- L2) by Def15; hence thesis by A1,A3,Th59; end; theorem Th82: L - L = ZeroLC(V) proof let v; thus (L - L).v = L.v - L.v by Th79 .= 0 by XCMPLX_1:14 .= ZeroLC(V).v by Th30; end; definition let V; func LinComb(V) -> set means :Def16: x in it iff x is Linear_Combination of V; existence proof defpred P[set] means $1 is Linear_Combination of V; consider A being set such that A1: for x holds x in A iff x in Funcs(the carrier of V, REAL) & P[x] from Separation; take A; let x; thus x in A implies x is Linear_Combination of V by A1; assume x is Linear_Combination of V; hence thesis by A1; end; uniqueness proof let D1,D2 be set; assume A2: for x holds x in D1 iff x is Linear_Combination of V; assume A3: for x holds x in D2 iff x is Linear_Combination of V; thus D1 c= D2 proof let x; assume x in D1; then x is Linear_Combination of V by A2; hence thesis by A3; end; let x; assume x in D2; then x is Linear_Combination of V by A3; hence thesis by A2; end; end; definition let V; cluster LinComb(V) -> non empty; coherence proof consider x being Linear_Combination of V; x in LinComb V by Def16; hence thesis; end; end; reserve e,e1,e2 for Element of LinComb(V); definition let V; let e; func @e -> Linear_Combination of V equals :Def17: e; coherence by Def16; end; definition let V; let L; func @L -> Element of LinComb(V) equals :Def18: L; coherence by Def16; end; definition let V; func LCAdd(V) -> BinOp of LinComb(V) means :Def19: for e1,e2 holds it.(e1,e2) = @e1 + @e2; existence proof deffunc F(Element of LinComb(V),Element of LinComb(V))=@(@$1 + @$2); consider o being BinOp of LinComb(V) such that A1: for e1,e2 holds o.(e1,e2) = F(e1,e2) from BinOpLambda; take o; let e1,e2; thus o.(e1,e2) = @(@e1 + @e2) by A1 .= @e1 + @e2 by Def18; end; uniqueness proof let o1,o2 be BinOp of LinComb(V); assume A2: for e1,e2 holds o1.(e1,e2) = @e1 + @e2; assume A3: for e1,e2 holds o2.(e1,e2) = @e1 + @e2; now let e1,e2; thus o1.(e1,e2) = @e1 + @e2 by A2 .= o2.(e1,e2) by A3; end; hence thesis by BINOP_1:2; end; end; definition let V; func LCMult(V) -> Function of [:REAL,LinComb(V):], LinComb(V) means :Def20: for a,e holds it.[a,e] = a * @e; existence proof defpred P[Element of REAL,Element of LinComb(V),set] means ex a st a = $1 & $3 = a * @$2; A1: for x being (Element of REAL), e1 ex e2 st P[x,e1,e2] proof let x be (Element of REAL), e1; take @(x * @e1); take x; thus thesis by Def18; end; consider g being Function of [:REAL,LinComb(V):], LinComb(V) such that A2: for x being (Element of REAL), e holds P[x,e,g.[x,e]] from FuncEx2D(A1); take g; let a,e; ex b st b = a & g.[a,e] = b * @e by A2; hence thesis; end; uniqueness proof let g1,g2 be Function of [:REAL,LinComb(V):], LinComb(V); assume A3: for a,e holds g1.[a,e] = a * @e; assume A4: for a,e holds g2.[a,e] = a * @e; now let x be (Element of REAL), e; thus g1.[x,e] = x * @e by A3 .= g2.[x,e] by A4; end; hence thesis by FUNCT_2:120; end; end; definition let V; func LC_RLSpace(V) -> RealLinearSpace equals :Def21: RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #); coherence proof set S = RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #); now let a,b be Real, v,u,w be VECTOR of S; A1: 0.S = @ZeroLC(V) by RLVECT_1:def 2 .= ZeroLC(V) by Def18; reconsider x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a * v, az = a * w, bx = b * v as Element of LinComb(V); @x = v & @y = u & @z = w & @yx = u + v & @xz = v + w & @ax = a * v & @az = a * w & @bx = b * v by Def17; then reconsider K = v, L = u, M = w, LK = u + v, KM = v + w, aK = a * v, aM = a * w, bK = b * v as Linear_Combination of V; A2: now let v,u be (VECTOR of S), K,L; assume A3: v = K & u = L; @K = K & @L = L by Def18; then A4: @@K = K & @@L = L by Def17; thus v + u = LCAdd(V).[v,u] by RLVECT_1:def 3 .= LCAdd(V).(K,L) by A3,BINOP_1:def 1 .= LCAdd(V).(@K,L) by Def18 .= LCAdd(V).(@K,@L) by Def18 .= K + L by A4,Def19; end; A5: now let v be (VECTOR of S), L,a; assume A6: v = L; @L = L by Def18; then A7: @@L = L by Def17; thus a * v = LCMult(V).[a,L] by A6,RLVECT_1:def 4 .= LCMult(V).[a,@L] by Def18 .= a * L by A7,Def20; end; thus v + w = K + M by A2 .= M + K by Th60 .= w + v by A2; thus (u + v) + w = LK + M by A2 .= L + K + M by A2 .= L + (K + M) by Th61 .= L + KM by A2 .= u + (v + w) by A2; thus v + 0.S = K + ZeroLC(V) by A1,A2 .= v by Th62; - K in the carrier of S by Def16; then - K in S by RLVECT_1:def 1; then - K = vector(S,- K) by Def1; then v + vector(S,- K) = K + (- K) by A2 .= K - K by Def15 .= 0.S by A1,Th82; hence ex w being VECTOR of S st v + w = 0.S; thus a * (v + w) = a * KM by A5 .= a * (K + M) by A2 .= a * K + a * M by Th69 .= aK + a * M by A5 .= aK + aM by A5 .= a * v + a * w by A2; thus (a + b) * v = (a + b) * K by A5 .= a * K + b * K by Th68 .= aK + b * K by A5 .= aK + bK by A5 .= a * v + b * v by A2; thus (a * b) * v = (a * b) * K by A5 .= a * (b * K) by Th70 .= a * (bK) by A5 .= a * (b * v) by A5; thus 1 * v = 1 * K by A5 .= v by Th71; end; then (for v,w being VECTOR of S holds v + w = w + v) & (for u,v,w being VECTOR of S holds (u + v) + w = u + (v + w)) & (for v being VECTOR of S holds v + 0.S = v) & (for v being VECTOR of S ex w being VECTOR of S st v + w = 0.S) & (for a for v,w being VECTOR of S holds a * (v + w) = a * v + a * w) & (for a,b for v being VECTOR of S holds (a + b) * v = a * v + b * v) & (for a,b for v being VECTOR of S holds (a * b) * v = a * (b * v)) & for v being VECTOR of S holds 1 * v = v; hence S is RealLinearSpace by RLVECT_1:7; end; end; definition let V; cluster LC_RLSpace(V) -> strict non empty; coherence proof LC_RLSpace(V) = RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #) by Def21; hence LC_RLSpace(V) is strict & the carrier of LC_RLSpace(V) is non empty; end; end; canceled 9; theorem Th92: the carrier of LC_RLSpace(V) = LinComb(V) proof LC_RLSpace(V) = RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #) by Def21; hence thesis; end; theorem the Zero of LC_RLSpace(V) = ZeroLC(V) proof LC_RLSpace(V) = RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #) by Def21; hence thesis by Def18; end; theorem Th94: the add of LC_RLSpace(V) = LCAdd(V) proof LC_RLSpace(V) = RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #) by Def21; hence thesis; end; theorem Th95: the Mult of LC_RLSpace(V) = LCMult(V) proof LC_RLSpace(V) = RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #) by Def21; hence thesis; end; theorem Th96: vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = L1 + L2 proof set v1 = vector(LC_RLSpace(V),L1); set v2 = vector(LC_RLSpace(V),L2); the carrier of LC_RLSpace(V) = LinComb(V) by Th92; then L1 in the carrier of LC_RLSpace(V) & L2 in the carrier of LC_RLSpace(V) by Def16; then A1: L1 in LC_RLSpace(V) & L2 in LC_RLSpace(V) by RLVECT_1:def 1; L1 = @L1 & L2 = @L2 by Def18; then A2: L1 = @@L1 & L2 = @@L2 by Def17; thus vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = (the add of LC_RLSpace(V)).[v1,v2] by RLVECT_1:def 3 .= LCAdd(V).[v1,v2] by Th94 .= LCAdd(V).[L1,v2] by A1,Def1 .= LCAdd(V).[L1,L2] by A1,Def1 .= LCAdd(V).[@L1,L2] by Def18 .= LCAdd(V).[@L1,@L2] by Def18 .= LCAdd(V).(@L1,@L2) by BINOP_1:def 1 .= L1 + L2 by A2,Def19; end; theorem Th97: a * vector(LC_RLSpace(V),L) = a * L proof the carrier of LC_RLSpace(V) = LinComb(V) by Th92; then L in the carrier of LC_RLSpace(V) by Def16; then A1: L in LC_RLSpace(V) by RLVECT_1:def 1; L = @L by Def18; then A2: @@L = L by Def17; the Mult of LC_RLSpace(V) = LCMult(V) by Th95; hence a * vector(LC_RLSpace(V),L) = LCMult(V).[a,vector(LC_RLSpace(V),L) ] by RLVECT_1:def 4 .= LCMult(V).[a,L] by A1,Def1 .= LCMult(V).[a,@L] by Def18 .= a * L by A2,Def20; end; theorem Th98: - vector(LC_RLSpace(V),L) = - L proof thus - vector(LC_RLSpace(V),L) = (- 1) * (vector(LC_RLSpace(V),L)) by RLVECT_1:29 .= (- 1) * L by Th97 .= - L by Def14; end; theorem vector(LC_RLSpace(V),L1) - vector(LC_RLSpace(V),L2) = L1 - L2 proof - L2 in LinComb(V) & the carrier of LC_RLSpace(V) = LinComb(V) by Def16,Th92; then A1: - L2 in LC_RLSpace(V) by RLVECT_1:def 1; - vector(LC_RLSpace(V),L2) = - L2 by Th98 .= vector(LC_RLSpace(V),- L2) by A1,Def1; hence vector(LC_RLSpace(V),L1) - vector(LC_RLSpace(V),L2) = vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),- L2) by RLVECT_1:def 11 .= L1 + (- L2) by Th96 .= L1 - L2 by Def15; end; definition let V; let A; func LC_RLSpace(A) -> strict Subspace of LC_RLSpace(V) means the carrier of it = {l : not contradiction}; existence proof set X = {l : not contradiction}; X c= the carrier of LC_RLSpace(V) proof let x; assume x in X; then ex l st x = l; then x in LinComb(V) by Def16; hence thesis by Th92; end; then reconsider X as Subset of LC_RLSpace(V); ZeroLC(V) is Linear_Combination of A by Th34; then A1: ZeroLC(V) in X; X is lineary-closed proof thus for v,u being VECTOR of LC_RLSpace(V) st v in X & u in X holds v + u in X proof let v,u be VECTOR of LC_RLSpace(V); assume that A2: v in X and A3: u in X; consider l1 such that A4: v = l1 by A2; consider l2 such that A5: u = l2 by A3; v = vector(LC_RLSpace(V),l1) & u = vector(LC_RLSpace(V),l2) by A4,A5,Th3; then v + u = l1 + l2 by Th96; then v + u is Linear_Combination of A by Th59; hence thesis; end; let a; let v be VECTOR of LC_RLSpace(V); assume v in X; then consider l such that A6: v = l; a * v = a * vector(LC_RLSpace(V),l) by A6,Th3 .= a * l by Th97; then a * v is Linear_Combination of A by Th67; hence thesis; end; hence thesis by A1,RLSUB_1:43; end; uniqueness by RLSUB_1:38; end; canceled 3; theorem k < n implies n - 1 is Nat by Lm1; canceled 3; theorem X is finite & Y is finite implies X \+\ Y is finite by Lm2; theorem for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds X = Y by Lm3;