let V be Z_Module; for W being Submodule of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let W be Submodule of V; for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let K be Linear_Combination of W; ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
defpred S1[ object , object ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0 ) );
reconsider K9 = K as Function of the carrier of W,INT ;
A1:
the carrier of W c= the carrier of V
by VECTSP_4:def 2;
then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1;
A2:
for x being object st x in the carrier of V holds
ex y being object st
( y in INT & S1[x,y] )
consider L being Function of the carrier of V,INT such that
A5:
for x being object st x in the carrier of V holds
S1[x,L . x]
from FUNCT_2:sch 1(A2);
L is Element of Funcs ( the carrier of V, the carrier of INT.Ring)
by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by A6, VECTSP_6:def 1;
reconsider L9 = L | the carrier of W as Function of the carrier of W,INT by A1, FUNCT_2:32;
take
L
; ( Carrier K = Carrier L & Sum K = Sum L )
then A11:
Carrier L c= the carrier of W
;
then
K9 = L9
by FUNCT_2:12;
hence
( Carrier K = Carrier L & Sum K = Sum L )
by A11, Th11; verum