let K be Ring; :: thesis: for X being VectSp of K ex I being Function of 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. () )

let X be VectSp of K; :: thesis: ex I being Function of 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. () )

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 () = len <*X*> by PRVECT_1:def 11;
then A2: len () = 1 by FINSEQ_1:40;
A3: dom <*X*> = {1} by ;
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 ;
then A5: carr <*X*> = <* the carrier of X*> by ;
then reconsider I = I as Function of 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
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 () ;
1 in {1} by TARSKI:def 1;
then reconsider j1 = 1 as Element of dom () by ;
A10: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_1:def 12;
A11: ([:():] . (Iv,Iw)) . j1 = (() . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def 8
.= v + w by ;
consider Ivw being Function such that
A12: ( (I . v) + (I . w) = Ivw & dom Ivw = dom () & ( for i being object st i in dom () holds
Ivw . i in () . i ) ) by CARD_3:def 5;
A13: dom Ivw = Seg 1 by ;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by ;
hence I . (v + w) = (I . v) + (I . w) by ; :: thesis: verum
end;
A14: for v being Vector of X
for r being Element of the carrier of K holds I . (r * v) = r * (I . v)
proof
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 () by ;
A17: (multop <*X*>) . j1 = the lmult of (<*X*> . j1) by Def8;
reconsider Iv = I . v as Element of product () ;
A18: ([:():] . (r,Iv)) . j1 = (() . j1) . (r,(Iv . j1)) by PRVECT_2:def 2
.= r * v by ;
consider Ivw being Function such that
A19: ( r * (I . v) = Ivw & dom Ivw = dom () & ( for i being object st i in dom () holds
Ivw . i in () . i ) ) by CARD_3:def 5;
A20: dom Ivw = Seg 1 by ;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by ;
hence I . (r * v) = r * (I . v) by ; :: thesis: verum
end;
I . (0. X) = I . ((0. X) + (0. X))
.= (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. ()) by RLVECT_1:15
.= I . (0. X) ;
hence ex I being Function of 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. () ) by ; :: thesis: verum