let V be free Z_Module; :: thesis: for X being Basis of V
for v being Vector of V st v in X & v <> 0. V holds
(Coordinate (v,X)) . v = 1
let X be Basis of V; :: thesis: for v being Vector of V st v in X & v <> 0. V holds
(Coordinate (v,X)) . v = 1
let v be Vector of V; :: thesis: ( v in X & v <> 0. V implies (Coordinate (v,X)) . v = 1 )
assume AS: ( v in X & v <> 0. V ) ; :: thesis: (Coordinate (v,X)) . v = 1
set f = Coordinate (v,X);
consider KL being Linear_Combination of X such that
A1: ( v = Sum KL & (Coordinate (v,X)) . v = KL . v ) by defCoord;
A3: Carrier KL c= X by VECTSP_6:def 4;
v in {v} by TARSKI:def 1;
then v in Lin {v} by ZMODUL02:65;
then consider Lb being Linear_Combination of {v} such that
A4: v = Sum Lb by ZMODUL02:64;
A7: Carrier Lb c= {v} by VECTSP_6:def 4;
{v} c= X by AS, ZFMISC_1:31;
then Carrier Lb c= X by A7;
then A9: Lb = KL by A4, A1, A3, Th5, VECTSP_7:def 3;
(Lb . v) * v = v by A4, ZMODUL02:21
.= (1. INT.Ring) * v by VECTSP_1:def 17 ;
hence (Coordinate (v,X)) . v = 1 by AS, A1, A9, ZMODUL01:11; :: thesis: verum