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 M2 = lmlt p,B2;
set M1 = lmlt p,B1;
A2: dom (lmlt p,B1) = (dom p) /\ (dom B1) by Lm1;
A3: 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 A4: i in dom (lmlt p,B1) ; :: thesis: (lmlt p,B1) . i = (lmlt p,B2) . i
i in dom p by A2, A4, XBOOLE_0:def 4;
then A5: p . i = p /. i by PARTFUN1:def 8;
A6: i in dom B1 by A2, A4, XBOOLE_0:def 4;
then A7: B2 . i = B2 /. i by A1, PARTFUN1:def 8;
A8: B1 . i = B1 /. i by A6, PARTFUN1:def 8;
hence (lmlt p,B1) . i = (p /. i) * (B1 /. i) by A4, A5, FUNCOP_1:28
.= (p /. i) * (B2 /. i) by A1, A6, A8, PARTFUN1:def 8, VECTSP_4:22
.= (lmlt p,B2) . i by A1, A2, A3, A4, A5, A7, FUNCOP_1:28 ;
:: thesis: verum

end;

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