let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1

for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

let b1 be OrdBasis of V1; :: thesis: for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

let d be FinSequence of K; :: thesis: ( len d = len b1 implies d = (Sum (lmlt (d,b1))) |-- b1 )

reconsider T = rng b1 as finite Subset of V1 by Def2;

defpred S_{1}[ Element of V1, Element of K] means ( ( $1 in rng b1 implies for k being Nat st k in dom b1 & b1 /. k = $1 holds

$2 = d /. k ) & ( not $1 in rng b1 implies $2 = 0. K ) );

A1: for v being Element of V1 ex u being Element of K st S_{1}[v,u]

A9: for v being Element of V1 holds S_{1}[v,KL . v]
from FUNCT_2:sch 3(A1);

then reconsider KL1 = KL as Linear_Combination of V1 by A10, VECTSP_6:def 1;

assume A11: len d = len b1 ; :: thesis: d = (Sum (lmlt (d,b1))) |-- b1

for b1 being OrdBasis of V1

for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1

for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

let b1 be OrdBasis of V1; :: thesis: for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

let d be FinSequence of K; :: thesis: ( len d = len b1 implies d = (Sum (lmlt (d,b1))) |-- b1 )

reconsider T = rng b1 as finite Subset of V1 by Def2;

defpred S

$2 = d /. k ) & ( not $1 in rng b1 implies $2 = 0. K ) );

A1: for v being Element of V1 ex u being Element of K st S

proof

consider KL being Function of V1,K such that
let v be Element of V1; :: thesis: ex u being Element of K st S_{1}[v,u]

end;per cases
( v in rng b1 or not v in rng b1 )
;

end;

suppose A2:
v in rng b1
; :: thesis: ex u being Element of K st S_{1}[v,u]

then consider k being Element of NAT such that

A3: k in dom b1 and

A4: b1 /. k = v by PARTFUN2:2;

take u = d /. k; :: thesis: S_{1}[v,u]

_{1}[v,u]
by A2; :: thesis: verum

end;A3: k in dom b1 and

A4: b1 /. k = v by PARTFUN2:2;

take u = d /. k; :: thesis: S

now :: thesis: for i being Nat st i in dom b1 & b1 /. i = v holds

u = d /. i

hence
Su = d /. i

A5:
b1 is one-to-one
by Def2;

let i be Nat; :: thesis: ( i in dom b1 & b1 /. i = v implies u = d /. i )

assume that

A6: i in dom b1 and

A7: b1 /. i = v ; :: thesis: u = d /. i

b1 . i = b1 /. k by A4, A6, A7, PARTFUN1:def 6

.= b1 . k by A3, PARTFUN1:def 6 ;

hence u = d /. i by A3, A6, A5, FUNCT_1:def 4; :: thesis: verum

end;let i be Nat; :: thesis: ( i in dom b1 & b1 /. i = v implies u = d /. i )

assume that

A6: i in dom b1 and

A7: b1 /. i = v ; :: thesis: u = d /. i

b1 . i = b1 /. k by A4, A6, A7, PARTFUN1:def 6

.= b1 . k by A3, PARTFUN1:def 6 ;

hence u = d /. i by A3, A6, A5, FUNCT_1:def 4; :: thesis: verum

A9: for v being Element of V1 holds S

A10: now :: thesis: ex T being finite Subset of V1 st

for v being Element of V1 st not v in T holds

KL . v = 0. K

for v being Element of V1 st not v in T holds

KL . v = 0. K

take T = T; :: thesis: for v being Element of V1 st not v in T holds

KL . v = 0. K

let v be Element of V1; :: thesis: ( not v in T implies KL . v = 0. K )

assume not v in T ; :: thesis: KL . v = 0. K

hence KL . v = 0. K by A9; :: thesis: verum

end;KL . v = 0. K

let v be Element of V1; :: thesis: ( not v in T implies KL . v = 0. K )

assume not v in T ; :: thesis: KL . v = 0. K

hence KL . v = 0. K by A9; :: thesis: verum

now :: thesis: ex f being Function of V1,K st

( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K )

then
KL in Funcs ( the carrier of V1, the carrier of K)
by FUNCT_2:def 2;( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K )

take f = KL; :: thesis: ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K )

thus ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum

end;thus ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum

then reconsider KL1 = KL as Linear_Combination of V1 by A10, VECTSP_6:def 1;

assume A11: len d = len b1 ; :: thesis: d = (Sum (lmlt (d,b1))) |-- b1

now :: thesis: ex KL1 being Linear_Combination of V1 st

( ( for k being Nat st 1 <= k & k <= len d holds

d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

hence
d = (Sum (lmlt (d,b1))) |-- b1
by A11, Def7; :: thesis: verum( ( for k being Nat st 1 <= k & k <= len d holds

d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

take KL1 = KL1; :: thesis: ( ( for k being Nat st 1 <= k & k <= len d holds

d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

A12: b1 is one-to-one by Def2;

thus A13: for k being Nat st 1 <= k & k <= len d holds

d /. k = KL1 . (b1 /. k) :: thesis: ( Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

x in rng b1

A17: dom d = dom b1 by A11, FINSEQ_3:29;

then A18: dom (lmlt (d,b1)) = dom b1 by Th12;

then A19: len (lmlt (d,b1)) = len b1 by FINSEQ_3:29

.= len (KL1 (#) b1) by VECTSP_6:def 5 ;

.= Sum KL1 by A16, A12, Th20 ;

:: thesis: verum

end;d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

A12: b1 is one-to-one by Def2;

thus A13: for k being Nat st 1 <= k & k <= len d holds

d /. k = KL1 . (b1 /. k) :: thesis: ( Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

proof

for x being object st x in Carrier KL1 holds
let k be Nat; :: thesis: ( 1 <= k & k <= len d implies d /. k = KL1 . (b1 /. k) )

assume ( 1 <= k & k <= len d ) ; :: thesis: d /. k = KL1 . (b1 /. k)

then A14: k in dom b1 by A11, FINSEQ_3:25;

then b1 . k = b1 /. k by PARTFUN1:def 6;

then b1 /. k in rng b1 by A14, FUNCT_1:def 3;

hence d /. k = KL1 . (b1 /. k) by A9, A14; :: thesis: verum

end;assume ( 1 <= k & k <= len d ) ; :: thesis: d /. k = KL1 . (b1 /. k)

then A14: k in dom b1 by A11, FINSEQ_3:25;

then b1 . k = b1 /. k by PARTFUN1:def 6;

then b1 /. k in rng b1 by A14, FUNCT_1:def 3;

hence d /. k = KL1 . (b1 /. k) by A9, A14; :: thesis: verum

x in rng b1

proof

hence A16:
Carrier KL1 c= rng b1
; :: thesis: Sum (lmlt (d,b1)) = Sum KL1
let x be object ; :: thesis: ( x in Carrier KL1 implies x in rng b1 )

assume x in Carrier KL1 ; :: thesis: x in rng b1

then A15: ex v being Element of V1 st

( x = v & KL1 . v <> 0. K ) by VECTSP_6:1;

assume not x in rng b1 ; :: thesis: contradiction

hence contradiction by A9, A15; :: thesis: verum

end;assume x in Carrier KL1 ; :: thesis: x in rng b1

then A15: ex v being Element of V1 st

( x = v & KL1 . v <> 0. K ) by VECTSP_6:1;

assume not x in rng b1 ; :: thesis: contradiction

hence contradiction by A9, A15; :: thesis: verum

A17: dom d = dom b1 by A11, FINSEQ_3:29;

then A18: dom (lmlt (d,b1)) = dom b1 by Th12;

then A19: len (lmlt (d,b1)) = len b1 by FINSEQ_3:29

.= len (KL1 (#) b1) by VECTSP_6:def 5 ;

now :: thesis: for k being Nat st k in dom (lmlt (d,b1)) holds

(lmlt (d,b1)) . k = (KL1 (#) b1) . k

hence Sum (lmlt (d,b1)) =
Sum (KL1 (#) b1)
by A19, FINSEQ_2:9
(lmlt (d,b1)) . k = (KL1 (#) b1) . k

let k be Nat; :: thesis: ( k in dom (lmlt (d,b1)) implies (lmlt (d,b1)) . k = (KL1 (#) b1) . k )

assume A20: k in dom (lmlt (d,b1)) ; :: thesis: (lmlt (d,b1)) . k = (KL1 (#) b1) . k

then A21: k in dom (KL1 (#) b1) by A19, FINSEQ_3:29;

A22: ( 1 <= k & k <= len d ) by A11, A18, A20, FINSEQ_3:25;

A23: ( d /. k = d . k & b1 /. k = b1 . k ) by A17, A18, A20, PARTFUN1:def 6;

thus (lmlt (d,b1)) . k = the lmult of V1 . ((d . k),(b1 . k)) by A20, FUNCOP_1:22

.= (d /. k) * (b1 /. k) by A23, VECTSP_1:def 12

.= (KL1 . (b1 /. k)) * (b1 /. k) by A13, A22

.= (KL1 (#) b1) . k by A21, VECTSP_6:def 5 ; :: thesis: verum

end;assume A20: k in dom (lmlt (d,b1)) ; :: thesis: (lmlt (d,b1)) . k = (KL1 (#) b1) . k

then A21: k in dom (KL1 (#) b1) by A19, FINSEQ_3:29;

A22: ( 1 <= k & k <= len d ) by A11, A18, A20, FINSEQ_3:25;

A23: ( d /. k = d . k & b1 /. k = b1 . k ) by A17, A18, A20, PARTFUN1:def 6;

thus (lmlt (d,b1)) . k = the lmult of V1 . ((d . k),(b1 . k)) by A20, FUNCOP_1:22

.= (d /. k) * (b1 /. k) by A23, VECTSP_1:def 12

.= (KL1 . (b1 /. k)) * (b1 /. k) by A13, A22

.= (KL1 (#) b1) . k by A21, VECTSP_6:def 5 ; :: thesis: verum

.= Sum KL1 by A16, A12, Th20 ;

:: thesis: verum