let V1 be free finite-rank Z_Module; :: thesis: for F being FinSequence of V1
for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL
let F be FinSequence of V1; :: thesis: for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL
let KL be Linear_Combination of V1; :: thesis: ( F is one-to-one & Carrier KL c= rng F implies Sum (KL (#) F) = Sum KL )
assume A1: F is one-to-one ; :: thesis: ( not Carrier KL c= rng F or Sum (KL (#) F) = Sum KL )
assume A2: Carrier KL c= rng F ; :: thesis: Sum (KL (#) F) = Sum KL
then reconsider A = Carrier KL as Subset of (rng F) ;
consider p1 being Permutation of (dom F) such that
A3: (F - (A `)) ^ (F - A) = F * p1 by FINSEQ_3:115;
reconsider G1 = F - (A `), G2 = F - A as FinSequence of V1 by FINSEQ_3:86;
A4: G1 is one-to-one by A1, FINSEQ_3:87;
len (KL (#) F) = len F by VECTSP_6:def 5;
then dom (KL (#) F) = dom F by FINSEQ_3:29;
then reconsider p1 = p1 as Permutation of (dom (KL (#) F)) ;
A5: rng G1 = (rng F) \ (A `) by FINSEQ_3:65
.= (rng F) /\ (Carrier KL) by XBOOLE_1:48
.= Carrier KL by A2, XBOOLE_1:28 ;
for k being Nat st k in dom (KL (#) G2) holds
(KL (#) G2) /. k = 0. V1
proof
let k be Nat; :: thesis: ( k in dom (KL (#) G2) implies (KL (#) G2) /. k = 0. V1 )
assume A6: k in dom (KL (#) G2) ; :: thesis: (KL (#) G2) /. k = 0. V1
len (KL (#) G2) = len G2 by VECTSP_6:def 5;
then A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29;
then G2 . k in rng G2 by A6, FUNCT_1:def 3;
then G2 . k in (rng F) \ (Carrier KL) by FINSEQ_3:65;
then not G2 . k in Carrier KL by XBOOLE_0:def 5;
then A8: not G2 /. k in Carrier KL by A6, A7, PARTFUN1:def 6;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
thus (KL (#) G2) /. k = (KL (#) G2) . k by A6, PARTFUN1:def 6
.= (KL . (G2 /. k1)) * (G2 /. k1) by A6, VECTSP_6:def 5
.= (0. INT.Ring) * (G2 /. k) by A8
.= 0. V1 by ZMODUL01:1 ; :: thesis: verum
end;
then A9: Sum (KL (#) G2) = 0. V1 by MATRLIN:11;
KL (#) (G1 ^ G2) = (KL (#) F) * p1 by A3, Th19;
hence Sum (KL (#) F) = Sum (KL (#) (G1 ^ G2)) by RLVECT_2:7
.= Sum ((KL (#) G1) ^ (KL (#) G2)) by ZMODUL02:51
.= (Sum (KL (#) G1)) + (Sum (KL (#) G2)) by RLVECT_1:41
.= Sum KL by A4, A5, A9, VECTSP_6:def 6 ;
:: thesis: verum