let V1 be free finite-rank Z_Module; :: thesis: for b1 being OrdBasis of V1
for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))
let b1 be OrdBasis of V1; :: thesis: for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))
let v be Element of V1; :: thesis: v = Sum (lmlt ((v |-- b1),b1))
consider KL being Linear_Combination of V1 such that
A1: ( v = Sum KL & Carrier KL c= rng b1 ) and
A2: for k being Nat st 1 <= k & k <= len (v |-- b1) holds
(v |-- b1) /. k = KL . (b1 /. k) by Def7;
len (v |-- b1) = len b1 by Def7;
then A3: dom (v |-- b1) = dom b1 by FINSEQ_3:29;
then A4: dom b1 = dom (lmlt ((v |-- b1),b1)) by Th12;
A51: len (KL (#) b1) = len b1 by VECTSP_6:def 5
.= len (lmlt ((v |-- b1),b1)) by A4, FINSEQ_3:29 ;
then A5: dom (KL (#) b1) = dom (lmlt ((v |-- b1),b1)) by FINSEQ_3:29;
A6: now :: thesis: for t being Nat st t in dom (lmlt ((v |-- b1),b1)) holds
(KL (#) b1) . t = (lmlt ((v |-- b1),b1)) . t
let t be Nat; :: thesis: ( t in dom (lmlt ((v |-- b1),b1)) implies (KL (#) b1) . t = (lmlt ((v |-- b1),b1)) . t )
assume A7: t in dom (lmlt ((v |-- b1),b1)) ; :: thesis: (KL (#) b1) . t = (lmlt ((v |-- b1),b1)) . t
then A8: b1 /. t = b1 . t by A4, PARTFUN1:def 6;
t in dom (v |-- b1) by A3, A7, Th12;
then A9: t <= len (v |-- b1) by FINSEQ_3:25;
A10: 1 <= t by A7, FINSEQ_3:25;
then A11: (v |-- b1) /. t = (v |-- b1) . t by A9, FINSEQ_4:15;
t in dom (KL (#) b1) by A51, A7, FINSEQ_3:29;
hence (KL (#) b1) . t = (KL . (b1 /. t)) * (b1 /. t) by VECTSP_6:def 5
.= ((v |-- b1) /. t) * (b1 /. t) by A2, A10, A9
.= (lmlt ((v |-- b1),b1)) . t by A7, A8, A11, FUNCOP_1:22 ;
:: thesis: verum
end;
thus v = Sum (KL (#) b1) by A1, defOrdBasis, Th20
.= Sum (lmlt ((v |-- b1),b1)) by A5, A6, FINSEQ_1:13 ; :: thesis: verum