let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for p being FinSequence of K
for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
lmlt p,B1 = lmlt p,B2
let V1 be finite-dimensional VectSp of K; :: thesis: for p being FinSequence of K
for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
lmlt p,B1 = lmlt p,B2
let p be FinSequence of K; :: thesis: for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
lmlt p,B1 = lmlt p,B2
let B1 be FinSequence of V1; :: thesis: for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
lmlt p,B1 = lmlt p,B2
let W1 be Subspace of V1; :: thesis: for B2 being FinSequence of W1 st B1 = B2 holds
lmlt p,B1 = lmlt p,B2
let B2 be FinSequence of W1; :: thesis: ( B1 = B2 implies lmlt p,B1 = lmlt p,B2 )
assume A1: B1 = B2 ; :: thesis: lmlt p,B1 = lmlt p,B2
set M1 = lmlt p,B1;
set M2 = lmlt p,B2;
A2: ( dom (lmlt p,B1) = (dom p) /\ (dom B1) & dom (lmlt p,B2) = (dom p) /\ (dom B2) ) by Lm1;

now

let i be Nat; :: thesis: ( i in dom (lmlt p,B1) implies (lmlt p,B1) . i = (lmlt p,B2) . i )
assume A3: i in dom (lmlt p,B1) ; :: thesis: (lmlt p,B1) . i = (lmlt p,B2) . i
( i in dom p & i in dom B1 ) by A2, A3, XBOOLE_0:def 4;
then A4: ( p . i = p /. i & B1 . i = B1 /. i & B2 . i = B2 /. i ) by A1, PARTFUN1:def 8;
hence (lmlt p,B1) . i = (p /. i) * (B1 /. i) by A3, FUNCOP_1:28
.= (p /. i) * (B2 /. i) by A1, A4, VECTSP_4:22
.= (lmlt p,B2) . i by A2, A3, A4, A1, FUNCOP_1:28 ;
:: thesis: verum

end;

hence lmlt p,B1 = lmlt p,B2 by A2, A1, FINSEQ_1:17; :: thesis: verum