let V2 be free finite-rank Z_Module; :: 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 A2, A5, XBOOLE_1:8;

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

let v be Vector of V2; :: thesis: KL1 . b₁ = KL2 . b₁

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

suppose A11: not v in (Carrier KL1) \/ (Carrier KL2) ; :: thesis: KL1 . b₁ = KL2 . b₁

then not v in Carrier KL2 by XBOOLE_0:def 3;
then A12: KL2 . v = 0 ;
not v in Carrier KL1 by A11, XBOOLE_0:def 3;
hence KL1 . v = KL2 . v by A12; :: thesis: verum

end;

suppose v in (Carrier KL1) \/ (Carrier KL2) ; :: thesis: KL1 . b₁ = KL2 . b₁

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;
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;

end;

end;

hence v1 = v2 by A1, A4, VECTSP_6:def 7; :: thesis: verum