let K be Ring; :: thesis: for X being VectSp of K ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

let X be VectSp of K; :: thesis: ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

set CarrX = the carrier of X;

consider I being Function of the carrier of X,(product <* the carrier of X*>) such that

A1: ( I is one-to-one & I is onto & ( for x being object st x in the carrier of X holds

I . x = <*x*> ) ) by PRVECT_3:4;

len (carr <*X*>) = len <*X*> by PRVECT_1:def 11;

then A2: len (carr <*X*>) = 1 by FINSEQ_1:40;

A3: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

A4: <*X*> . 1 = X by FINSEQ_1:def 8;

1 in {1} by TARSKI:def 1;

then (carr <*X*>) . 1 = the carrier of X by A3, A4, PRVECT_1:def 11;

then A5: carr <*X*> = <* the carrier of X*> by A2, FINSEQ_1:40;

then reconsider I = I as Function of X,(product <*X*>) ;

A6: for x being Vector of X holds I . x = <*x*> by A1;

A7: for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w)

for r being Element of the carrier of K holds I . (r * v) = r * (I . v)

.= (I . (0. X)) + (I . (0. X)) by A7 ;

then (I . (0. X)) - (I . (0. X)) = (I . (0. X)) + ((I . (0. X)) - (I . (0. X))) by RLVECT_1:28

.= (I . (0. X)) + (0. (product <*X*>)) by RLVECT_1:15

.= I . (0. X) ;

hence ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) ) by A1, A6, A5, A7, A14, RLVECT_1:15; :: thesis: verum

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

let X be VectSp of K; :: thesis: ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

set CarrX = the carrier of X;

consider I being Function of the carrier of X,(product <* the carrier of X*>) such that

A1: ( I is one-to-one & I is onto & ( for x being object st x in the carrier of X holds

I . x = <*x*> ) ) by PRVECT_3:4;

len (carr <*X*>) = len <*X*> by PRVECT_1:def 11;

then A2: len (carr <*X*>) = 1 by FINSEQ_1:40;

A3: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

A4: <*X*> . 1 = X by FINSEQ_1:def 8;

1 in {1} by TARSKI:def 1;

then (carr <*X*>) . 1 = the carrier of X by A3, A4, PRVECT_1:def 11;

then A5: carr <*X*> = <* the carrier of X*> by A2, FINSEQ_1:40;

then reconsider I = I as Function of X,(product <*X*>) ;

A6: for x being Vector of X holds I . x = <*x*> by A1;

A7: for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w)

proof

A14:
for v being Vector of X
let v, w be Vector of X; :: thesis: I . (v + w) = (I . v) + (I . w)

A8: ( I . v = <*v*> & I . w = <*w*> & I . (v + w) = <*(v + w)*> ) by A1;

A9: ( <*v*> . 1 = v & <*w*> . 1 = w ) by FINSEQ_1:40;

reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X*>) ;

1 in {1} by TARSKI:def 1;

then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;

A10: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_1:def 12;

A11: ([:(addop <*X*>):] . (Iv,Iw)) . j1 = ((addop <*X*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8

.= v + w by A10, A8, A9, FINSEQ_1:40 ;

consider Ivw being Function such that

A12: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being object st i in dom (carr <*X*>) holds

Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def 5;

A13: dom Ivw = Seg 1 by A2, A12, FINSEQ_1:def 3;

then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;

len Ivw = 1 by A13, FINSEQ_1:def 3;

hence I . (v + w) = (I . v) + (I . w) by A8, A12, A11, FINSEQ_1:40; :: thesis: verum

end;A8: ( I . v = <*v*> & I . w = <*w*> & I . (v + w) = <*(v + w)*> ) by A1;

A9: ( <*v*> . 1 = v & <*w*> . 1 = w ) by FINSEQ_1:40;

reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X*>) ;

1 in {1} by TARSKI:def 1;

then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;

A10: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_1:def 12;

A11: ([:(addop <*X*>):] . (Iv,Iw)) . j1 = ((addop <*X*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8

.= v + w by A10, A8, A9, FINSEQ_1:40 ;

consider Ivw being Function such that

A12: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being object st i in dom (carr <*X*>) holds

Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def 5;

A13: dom Ivw = Seg 1 by A2, A12, FINSEQ_1:def 3;

then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;

len Ivw = 1 by A13, FINSEQ_1:def 3;

hence I . (v + w) = (I . v) + (I . w) by A8, A12, A11, FINSEQ_1:40; :: thesis: verum

for r being Element of the carrier of K holds I . (r * v) = r * (I . v)

proof

I . (0. X) =
I . ((0. X) + (0. X))
let v be Vector of X; :: thesis: for r being Element of the carrier of K holds I . (r * v) = r * (I . v)

let r be Element of the carrier of K; :: thesis: I . (r * v) = r * (I . v)

A15: ( I . v = <*v*> & I . (r * v) = <*(r * v)*> ) by A1;

A16: <*v*> . 1 = v by FINSEQ_1:40;

1 in {1} by TARSKI:def 1;

then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;

A17: (multop <*X*>) . j1 = the lmult of (<*X*> . j1) by Def8;

reconsider Iv = I . v as Element of product (carr <*X*>) ;

A18: ([:(multop <*X*>):] . (r,Iv)) . j1 = ((multop <*X*>) . j1) . (r,(Iv . j1)) by PRVECT_2:def 2

.= r * v by A17, A15, A16, FINSEQ_1:40 ;

consider Ivw being Function such that

A19: ( r * (I . v) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being object st i in dom (carr <*X*>) holds

Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def 5;

A20: dom Ivw = Seg 1 by A2, A19, FINSEQ_1:def 3;

then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;

len Ivw = 1 by A20, FINSEQ_1:def 3;

hence I . (r * v) = r * (I . v) by A15, A19, A18, FINSEQ_1:40; :: thesis: verum

end;let r be Element of the carrier of K; :: thesis: I . (r * v) = r * (I . v)

A15: ( I . v = <*v*> & I . (r * v) = <*(r * v)*> ) by A1;

A16: <*v*> . 1 = v by FINSEQ_1:40;

1 in {1} by TARSKI:def 1;

then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;

A17: (multop <*X*>) . j1 = the lmult of (<*X*> . j1) by Def8;

reconsider Iv = I . v as Element of product (carr <*X*>) ;

A18: ([:(multop <*X*>):] . (r,Iv)) . j1 = ((multop <*X*>) . j1) . (r,(Iv . j1)) by PRVECT_2:def 2

.= r * v by A17, A15, A16, FINSEQ_1:40 ;

consider Ivw being Function such that

A19: ( r * (I . v) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being object st i in dom (carr <*X*>) holds

Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def 5;

A20: dom Ivw = Seg 1 by A2, A19, FINSEQ_1:def 3;

then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;

len Ivw = 1 by A20, FINSEQ_1:def 3;

hence I . (r * v) = r * (I . v) by A15, A19, A18, FINSEQ_1:40; :: thesis: verum

.= (I . (0. X)) + (I . (0. X)) by A7 ;

then (I . (0. X)) - (I . (0. X)) = (I . (0. X)) + ((I . (0. X)) - (I . (0. X))) by RLVECT_1:28

.= (I . (0. X)) + (0. (product <*X*>)) by RLVECT_1:15

.= I . (0. X) ;

hence ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) ) by A1, A6, A5, A7, A14, RLVECT_1:15; :: thesis: verum