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
A8: now :: thesis: for t being Nat st 1 <= t & t <= len (v1 |-- b2) holds
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;
A10: (Carrier KL1) \/ (Carrier KL2) c= rng b2 by ;
now :: thesis: for v being Vector of V2 holds KL1 . v = KL2 . v
let v be Vector of V2; :: thesis: KL1 . b1 = KL2 . b1
per cases ( not v in (Carrier KL1) \/ (Carrier KL2) or v in (Carrier KL1) \/ (Carrier KL2) ) ;
suppose v in (Carrier KL1) \/ (Carrier KL2) ; :: thesis: KL1 . b1 = KL2 . b1
then consider x being object such that
A13: x in dom b2 and
A14: v = b2 . x by ;
reconsider x = x as Nat by ;
x <= len b2 by ;
then A15: x <= len (v1 |-- b2) by Def7;
( v = b2 /. x & 1 <= x ) by ;
hence KL1 . v = KL2 . v by ; :: thesis: verum
end;
end;
end;
hence v1 = v2 by ; :: thesis: verum