let K be Field; :: thesis: for V2 being finite-dimensional VectSp of K

for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

let V2 be finite-dimensional VectSp of K; :: thesis: for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

let b2 be OrdBasis of V2; :: thesis: for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

let v1, v2 be Vector of V2; :: thesis: ( v1 |-- b2 = v2 |-- b2 implies v1 = v2 )

consider KL1 being Linear_Combination of V2 such that

A1: v1 = Sum KL1 and

A2: Carrier KL1 c= rng b2 and

A3: for t being Nat st 1 <= t & t <= len (v1 |-- b2) holds

(v1 |-- b2) /. t = KL1 . (b2 /. t) by Def7;

consider KL2 being Linear_Combination of V2 such that

A4: v2 = Sum KL2 and

A5: Carrier KL2 c= rng b2 and

A6: for t being Nat st 1 <= t & t <= len (v2 |-- b2) holds

(v2 |-- b2) /. t = KL2 . (b2 /. t) by Def7;

assume A7: v1 |-- b2 = v2 |-- b2 ; :: thesis: v1 = v2

for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

let V2 be finite-dimensional VectSp of K; :: thesis: for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

let b2 be OrdBasis of V2; :: thesis: for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

let v1, v2 be Vector of V2; :: thesis: ( v1 |-- b2 = v2 |-- b2 implies v1 = v2 )

consider KL1 being Linear_Combination of V2 such that

A1: v1 = Sum KL1 and

A2: Carrier KL1 c= rng b2 and

A3: for t being Nat st 1 <= t & t <= len (v1 |-- b2) holds

(v1 |-- b2) /. t = KL1 . (b2 /. t) by Def7;

consider KL2 being Linear_Combination of V2 such that

A4: v2 = Sum KL2 and

A5: Carrier KL2 c= rng b2 and

A6: for t being Nat st 1 <= t & t <= len (v2 |-- b2) holds

(v2 |-- b2) /. t = KL2 . (b2 /. t) by Def7;

assume A7: v1 |-- b2 = v2 |-- b2 ; :: thesis: v1 = v2

A8: now :: thesis: for t being Nat st 1 <= t & t <= len (v1 |-- b2) holds

KL1 . (b2 /. t) = KL2 . (b2 /. t)

A10:
(Carrier KL1) \/ (Carrier KL2) c= rng b2
by A2, A5, XBOOLE_1:8;KL1 . (b2 /. t) = KL2 . (b2 /. t)

let t be Nat; :: thesis: ( 1 <= t & t <= len (v1 |-- b2) implies KL1 . (b2 /. t) = KL2 . (b2 /. t) )

assume A9: ( 1 <= t & t <= len (v1 |-- b2) ) ; :: thesis: KL1 . (b2 /. t) = KL2 . (b2 /. t)

hence KL1 . (b2 /. t) = (v2 |-- b2) /. t by A7, A3

.= KL2 . (b2 /. t) by A7, A6, A9 ;

:: thesis: verum

end;assume A9: ( 1 <= t & t <= len (v1 |-- b2) ) ; :: thesis: KL1 . (b2 /. t) = KL2 . (b2 /. t)

hence KL1 . (b2 /. t) = (v2 |-- b2) /. t by A7, A3

.= KL2 . (b2 /. t) by A7, A6, A9 ;

:: thesis: verum

now :: thesis: for v being Vector of V2 holds KL1 . v = KL2 . v

hence
v1 = v2
by A1, A4, VECTSP_6:def 7; :: thesis: verumlet v be Vector of V2; :: thesis: KL1 . b_{1} = KL2 . b_{1}

end;per cases
( not v in (Carrier KL1) \/ (Carrier KL2) or v in (Carrier KL1) \/ (Carrier KL2) )
;

end;

suppose A11:
not v in (Carrier KL1) \/ (Carrier KL2)
; :: thesis: KL1 . b_{1} = KL2 . b_{1}

then
not v in Carrier KL2
by XBOOLE_0:def 3;

then A12: KL2 . v = 0. K by VECTSP_6:2;

not v in Carrier KL1 by A11, XBOOLE_0:def 3;

hence KL1 . v = KL2 . v by A12, VECTSP_6:2; :: thesis: verum

end;then A12: KL2 . v = 0. K by VECTSP_6:2;

not v in Carrier KL1 by A11, XBOOLE_0:def 3;

hence KL1 . v = KL2 . v by A12, VECTSP_6:2; :: thesis: verum

suppose
v in (Carrier KL1) \/ (Carrier KL2)
; :: thesis: KL1 . b_{1} = KL2 . b_{1}

then consider x being object such that

A13: x in dom b2 and

A14: v = b2 . x by A10, FUNCT_1:def 3;

reconsider x = x as Nat by A13, FINSEQ_3:23;

x <= len b2 by A13, FINSEQ_3:25;

then A15: x <= len (v1 |-- b2) by Def7;

( v = b2 /. x & 1 <= x ) by A13, A14, FINSEQ_3:25, PARTFUN1:def 6;

hence KL1 . v = KL2 . v by A8, A15; :: thesis: verum

end;A13: x in dom b2 and

A14: v = b2 . x by A10, FUNCT_1:def 3;

reconsider x = x as Nat by A13, FINSEQ_3:23;

x <= len b2 by A13, FINSEQ_3:25;

then A15: x <= len (v1 |-- b2) by Def7;

( v = b2 /. x & 1 <= x ) by A13, A14, FINSEQ_3:25, PARTFUN1:def 6;

hence KL1 . v = KL2 . v by A8, A15; :: thesis: verum