let V be Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of ()
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = () .: I & l = lq * () holds
Sum lq = () . (Sum l)

let I be Subset of V; :: thesis: for IQ being Subset of ()
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = () .: I & l = lq * () holds
Sum lq = () . (Sum l)

let IQ be Subset of (); :: thesis: for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = () .: I & l = lq * () holds
Sum lq = () . (Sum l)

let l be Linear_Combination of I; :: thesis: for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = () .: I & l = lq * () holds
Sum lq = () . (Sum l)

let lq be Linear_Combination of IQ; :: thesis: ( V is Mult-cancelable & IQ = () .: I & l = lq * () implies Sum lq = () . (Sum l) )
assume AS0: ( V is Mult-cancelable & IQ = () .: I & l = lq * () ) ; :: thesis: Sum lq = () . (Sum l)
per cases ( I is empty or not I is empty ) ;
suppose A3: I is empty ; :: thesis: Sum lq = () . (Sum l)
then IQ = {} the carrier of () by AS0;
then lq = ZeroLC () by VECTSP_6:6;
then A6: Sum lq = 0. () by VECTSP_6:15;
I = {} the carrier of V by A3;
then l = ZeroLC V by ZMODUL02:12;
then Sum l = 0. V by ZMODUL02:19;
hence Sum lq = () . (Sum l) by ; :: thesis: verum
end;
suppose E1: not I is empty ; :: thesis: Sum lq = () . (Sum l)
then consider v0 being object such that
A7: v0 in I ;
reconsider v0 = v0 as Vector of V by A7;
(MorphsZQ V) . v0 in IQ by ;
then reconsider X = IQ as non empty Subset of () ;
reconsider g = () | I as Function of I,IQ by ;
MorphsZQ V is one-to-one by ;
then AX1: g is one-to-one by FUNCT_1:52;
AX2: rng g = IQ by ;
then reconsider F = g " as Function of IQ,I by ;
reconsider F = F as Function of X, the carrier of V by ;
X = IQ ;
then AX2A: dom g = I by FUNCT_2:def 1;
then AX3: ( dom F = X & rng F = I ) by ;
A8: for u being Vector of V st u in I holds
F . (() . u) = u
proof
let u be Vector of V; :: thesis: ( u in I implies F . (() . u) = u )
assume AS8: u in I ; :: thesis: F . (() . u) = u
hence F . (() . u) = F . (g . u) by FUNCT_1:49
.= u by ;
:: thesis: verum
end;
consider Gq being FinSequence of () such that
A9: ( Gq is one-to-one & rng Gq = Carrier lq & Sum lq = Sum (lq (#) Gq) ) by VECTSP_6:def 6;
set n = len Gq;
A10: dom Gq = Seg (len Gq) by FINSEQ_1:def 3;
A11: Carrier lq c= X by VECTSP_6:def 4;
A12: dom (F * Gq) = Seg (len Gq) by ;
A13: rng (F * Gq) c= the carrier of V ;
F * Gq is FinSequence by ;
then reconsider FGq = F * Gq as FinSequence of V by ;
for x being object holds
( x in rng FGq iff x in Carrier l )
proof
let x be object ; :: thesis: ( x in rng FGq iff x in Carrier l )
hereby :: thesis: ( x in Carrier l implies x in rng FGq )
assume x in rng FGq ; :: thesis:
then consider z being object such that
A14: ( z in dom FGq & x = FGq . z ) by FUNCT_1:def 3;
A15: x = F . (Gq . z) by ;
A16: ( z in dom Gq & Gq . z in dom F ) by ;
then consider u being Vector of V such that
A17: ( u in I & Gq . z = () . u ) by ;
A18: F . (Gq . z) = u by ;
consider w being Element of () such that
A19: ( Gq . z = w & lq . w <> 0. F_Rat ) by ;
l . u <> 0. F_Rat by ;
hence x in Carrier l by ; :: thesis: verum
end;
assume A20: x in Carrier l ; :: thesis: x in rng FGq
then reconsider u = x as Vector of V ;
A21: l . u <> 0 by ;
A22: Carrier l c= I by VECTSP_6:def 4;
lq . (() . u) <> 0 by ;
then A23: (MorphsZQ V) . u in rng Gq by A9;
then consider z being object such that
A24: ( z in dom Gq & () . u = Gq . z ) by FUNCT_1:def 3;
A25: F . (Gq . z) = u by A20, A22, A24, A8;
A26: z in dom FGq by ;
then FGq . z = u by ;
hence x in rng FGq by ; :: thesis: verum
end;
then rng FGq = Carrier l by TARSKI:2;
then A27: Sum l = Sum (l (#) FGq) by ;
A28: len (l (#) FGq) = len FGq by VECTSP_6:def 5;
then A29: len (l (#) FGq) = len Gq by ;
A30: len (lq (#) Gq) = len Gq by VECTSP_6:def 5;
now :: thesis: for i being Element of NAT st i in dom (l (#) FGq) holds
ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = () . si )
let i be Element of NAT ; :: thesis: ( i in dom (l (#) FGq) implies ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = () . si ) )

assume A31: i in dom (l (#) FGq) ; :: thesis: ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = () . si )

then i in Seg (len FGq) by ;
then A32: i in dom FGq by FINSEQ_1:def 3;
then FGq . i in rng FGq by FUNCT_1:3;
then reconsider v = FGq . i as Element of V ;
A33: (l (#) FGq) . i = (l . v) * v by ;
i in Seg (len Gq) by ;
then A34: i in dom Gq by FINSEQ_1:def 3;
then A35: Gq . i in rng Gq by FUNCT_1:3;
reconsider w = Gq . i as Element of () by A35;
consider u being Vector of V such that
A37: ( u in I & Gq . i = () . u ) by ;
A381: F . (Gq . i) = u by ;
then A38: v = u by ;
A39: w = () . v by ;
A40: lq . w = l . v by ;
T1: (lq . w) * w = () . ((l . v) * v) by ;
thus ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = () . si ) :: thesis: verum
proof
take si = (l (#) FGq) . i; :: thesis: ( si is VECTOR of V & si = (l (#) FGq) . i & (lq (#) Gq) . i = () . si )
thus ( si is VECTOR of V & si = (l (#) FGq) . i & (lq (#) Gq) . i = () . si ) by ; :: thesis: verum
end;
end;
hence Sum lq = () . (Sum l) by A9, A27, A29, A30, AS0, XThSum; :: thesis: verum
end;
end;