let K be Field; for V1, V2 being VectSp of K
for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let V1, V2 be VectSp of K; for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let A be Subset of V1; for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let L be Linear_Combination of V2; for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L
let f be linear-transformation of V1,V2; ( Carrier L c= f .: A implies ex M being Linear_Combination of A st f . (Sum M) = Sum L )
assume A1:
Carrier L c= f .: A
; ex M being Linear_Combination of A st f . (Sum M) = Sum L
set C = Carrier L;
consider F being FinSequence of the carrier of V2 such that
A2:
F is one-to-one
and
A3:
rng F = Carrier L
and
A4:
Sum L = Sum (L (#) F)
by VECTSP_6:def 6;
defpred S1[ object , object ] means ( $2 in A & f . $2 = F . $1 );
set D = dom F;
A5:
for x being object st x in dom F holds
ex y being object st
( y in the carrier of V1 & S1[x,y] )
consider p being Function of (dom F), the carrier of V1 such that
A7:
for x being object st x in dom F holds
S1[x,p . x]
from FUNCT_2:sch 1(A5);
A8:
rng p c= the carrier of V1
by RELAT_1:def 19;
A9:
dom p = dom F
by FUNCT_2:def 1;
dom F = Seg (len F)
by FINSEQ_1:def 3;
then reconsider p = p as FinSequence by A9, FINSEQ_1:def 2;
reconsider p = p as FinSequence of V1 by A8, FINSEQ_1:def 4;
then A13:
p is one-to-one
by FUNCT_1:def 4;
reconsider RNG = rng p as finite Subset of V1 by RELAT_1:def 19;
defpred S2[ object , object ] means ( ( $1 in rng p implies for x being set st x in dom F & p . x = $1 holds
$2 = L . (F . x) ) & ( not $1 in rng p implies $2 = 0. K ) );
A14:
for x being object st x in the carrier of V1 holds
ex y being object st
( y in the carrier of K & S2[x,y] )
consider M being Function of V1,K such that
A18:
for x being object st x in the carrier of V1 holds
S2[x,M . x]
from FUNCT_2:sch 1(A14);
reconsider M = M as Element of Funcs ( the carrier of V1, the carrier of K) by FUNCT_2:8;
for v1 being Element of V1 st not v1 in RNG holds
M . v1 = 0. K
by A18;
then reconsider M = M as Linear_Combination of V1 by VECTSP_6:def 1;
A19:
Carrier M = RNG
RNG c= A
then reconsider M = M as Linear_Combination of A by A19, VECTSP_6:def 4;
len (M (#) p) = len p
by VECTSP_6:def 5;
then A25:
dom (M (#) p) = dom F
by A9, FINSEQ_3:29;
len (L (#) F) = len F
by VECTSP_6:def 5;
then A26:
dom (L (#) F) = dom F
by FINSEQ_3:29;
A27:
now for x being object st x in dom F holds
(f * (M (#) p)) . x = (L (#) F) . xlet x be
object ;
( x in dom F implies (f * (M (#) p)) . x = (L (#) F) . x )assume A28:
x in dom F
;
(f * (M (#) p)) . x = (L (#) F) . xreconsider i =
x as
Element of
NAT by A28;
A29:
F . i = F /. i
by A28, PARTFUN1:def 6;
p . i in RNG
by A9, A28, FUNCT_1:def 3;
then A30:
M . (p . i) = L . (F . i)
by A18, A28;
A31:
(
p /. i = p . i &
f . (p . i) = F . i )
by A7, A9, A28, PARTFUN1:def 6;
thus (f * (M (#) p)) . x =
f . ((M (#) p) . i)
by A25, A28, FUNCT_1:13
.=
f . ((M . (p /. i)) * (p /. i))
by A25, A28, VECTSP_6:def 5
.=
(L . (F /. i)) * (F /. i)
by A31, A29, A30, MOD_2:def 2
.=
(L (#) F) . x
by A26, A28, VECTSP_6:def 5
;
verum end;
take
M
; f . (Sum M) = Sum L
( dom f = [#] V1 & rng (M (#) p) c= [#] V1 )
by FUNCT_2:def 1, RELAT_1:def 19;
then
dom (f * (M (#) p)) = dom (M (#) p)
by RELAT_1:27;
then
f * (M (#) p) = L (#) F
by A26, A25, A27, FUNCT_1:2;
hence Sum L =
f . (Sum (M (#) p))
by A4, MATRLIN:16
.=
f . (Sum M)
by A13, A19, VECTSP_6:def 6
;
verum