let V be Z_Module; :: thesis: for L being Linear_Combination of V

for F being FinSequence of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

let F be FinSequence of V; :: thesis: ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

defpred S_{1}[ object , object ] means ( not $1 is Vector of V or ( $1 in rng F & $2 = L . $1 ) or ( not $1 in rng F & $2 = 0 ) );

reconsider R = rng F as finite Subset of V ;

A1: for x being object st x in the carrier of V holds

ex y being object st

( y in INT & S_{1}[x,y] )

for x being object st x in the carrier of V holds

S_{1}[x,K . x]
from FUNCT_2:sch 1(A1);

then consider K being Function of the carrier of V,INT such that

A4: for x being object st x in the carrier of V holds

S_{1}[x,K . x]
;

reconsider K = K as Linear_Combination of V by A5, VECTSP_6:def 1;

take K ; :: thesis: ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

A10: L (#) F = K (#) F

hence ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) by A9, A10, XBOOLE_0:def 10; :: thesis: verum

for F being FinSequence of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

let F be FinSequence of V; :: thesis: ex K being Linear_Combination of V st

( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

defpred S

reconsider R = rng F as finite Subset of V ;

A1: for x being object st x in the carrier of V holds

ex y being object st

( y in INT & S

proof

ex K being Function of the carrier of V,INT st
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in INT & S_{1}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in INT & S_{1}[x,y] )

then reconsider x9 = x as Vector of V ;

end;( y in INT & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in INT & S

then reconsider x9 = x as Vector of V ;

for x being object st x in the carrier of V holds

S

then consider K being Function of the carrier of V,INT such that

A4: for x being object st x in the carrier of V holds

S

A5: now :: thesis: for v being Vector of V st not v in R /\ (Carrier L) holds

K . v = 0

reconsider K = K as Element of Funcs ( the carrier of V,INT) by FUNCT_2:8;K . v = 0

let v be Vector of V; :: thesis: ( not v in R /\ (Carrier L) implies K . b_{1} = 0 )

assume A6: not v in R /\ (Carrier L) ; :: thesis: K . b_{1} = 0

end;assume A6: not v in R /\ (Carrier L) ; :: thesis: K . b

reconsider K = K as Linear_Combination of V by A5, VECTSP_6:def 1;

now :: thesis: for v being object st v in (rng F) /\ (Carrier L) holds

v in Carrier K

then A9:
(rng F) /\ (Carrier L) c= Carrier K
;v in Carrier K

let v be object ; :: thesis: ( v in (rng F) /\ (Carrier L) implies v in Carrier K )

assume A7: v in (rng F) /\ (Carrier L) ; :: thesis: v in Carrier K

then reconsider v9 = v as Vector of V ;

v in Carrier L by A7, XBOOLE_0:def 4;

then A8: L . v9 <> 0 by ZMODUL02:8;

v in R by A7, XBOOLE_0:def 4;

then K . v9 = L . v9 by A4;

hence v in Carrier K by A8; :: thesis: verum

end;assume A7: v in (rng F) /\ (Carrier L) ; :: thesis: v in Carrier K

then reconsider v9 = v as Vector of V ;

v in Carrier L by A7, XBOOLE_0:def 4;

then A8: L . v9 <> 0 by ZMODUL02:8;

v in R by A7, XBOOLE_0:def 4;

then K . v9 = L . v9 by A4;

hence v in Carrier K by A8; :: thesis: verum

take K ; :: thesis: ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

A10: L (#) F = K (#) F

proof

set p = L (#) F;

set q = K (#) F;

A11: len (L (#) F) = len F by VECTSP_6:def 5;

len (K (#) F) = len F by VECTSP_6:def 5;

then A12: dom (L (#) F) = dom (K (#) F) by A11, FINSEQ_3:29;

A13: dom (L (#) F) = dom F by A11, FINSEQ_3:29;

end;set q = K (#) F;

A11: len (L (#) F) = len F by VECTSP_6:def 5;

len (K (#) F) = len F by VECTSP_6:def 5;

then A12: dom (L (#) F) = dom (K (#) F) by A11, FINSEQ_3:29;

A13: dom (L (#) F) = dom F by A11, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom (L (#) F) holds

(L (#) F) . k = (K (#) F) . k

hence
L (#) F = K (#) F
by A12, FINSEQ_1:13; :: thesis: verum(L (#) F) . k = (K (#) F) . k

let k be Nat; :: thesis: ( k in dom (L (#) F) implies (L (#) F) . k = (K (#) F) . k )

set u = F /. k;

A14: S_{1}[F /. k,K . (F /. k)]
by A4;

assume A15: k in dom (L (#) F) ; :: thesis: (L (#) F) . k = (K (#) F) . k

then ( F /. k = F . k & (L (#) F) . k = (L . (F /. k)) * (F /. k) ) by A13, PARTFUN1:def 6, VECTSP_6:def 5;

hence (L (#) F) . k = (K (#) F) . k by A12, A13, A15, A14, FUNCT_1:def 3, VECTSP_6:def 5; :: thesis: verum

end;set u = F /. k;

A14: S

assume A15: k in dom (L (#) F) ; :: thesis: (L (#) F) . k = (K (#) F) . k

then ( F /. k = F . k & (L (#) F) . k = (L . (F /. k)) * (F /. k) ) by A13, PARTFUN1:def 6, VECTSP_6:def 5;

hence (L (#) F) . k = (K (#) F) . k by A12, A13, A15, A14, FUNCT_1:def 3, VECTSP_6:def 5; :: thesis: verum

now :: thesis: for v being object st v in Carrier K holds

v in (rng F) /\ (Carrier L)

then
Carrier K c= (rng F) /\ (Carrier L)
;v in (rng F) /\ (Carrier L)

let v be object ; :: thesis: ( v in Carrier K implies v in (rng F) /\ (Carrier L) )

assume v in Carrier K ; :: thesis: v in (rng F) /\ (Carrier L)

then ex v9 being Vector of V st

( v9 = v & K . v9 <> 0 ) ;

hence v in (rng F) /\ (Carrier L) by A5; :: thesis: verum

end;assume v in Carrier K ; :: thesis: v in (rng F) /\ (Carrier L)

then ex v9 being Vector of V st

( v9 = v & K . v9 <> 0 ) ;

hence v in (rng F) /\ (Carrier L) by A5; :: thesis: verum

hence ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) by A9, A10, XBOOLE_0:def 10; :: thesis: verum