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 :: thesis: for i being Nat st i in dom (lmlt (p,B1)) holds
(lmlt (p,B1)) . i = (lmlt (p,B2)) . i
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 6;
A6: i in dom B1 by A2, A4, XBOOLE_0:def 4;
then A7: B2 . i = B2 /. i by A1, PARTFUN1:def 6;
A8: B1 . i = B1 /. i by A6, PARTFUN1:def 6;
hence (lmlt (p,B1)) . i = (p /. i) * (B1 /. i) by A4, A5, FUNCOP_1:22
.= (p /. i) * (B2 /. i) by A1, A6, A8, PARTFUN1:def 6, VECTSP_4:14
.= (lmlt (p,B2)) . i by A1, A2, A3, A4, A5, A7, FUNCOP_1:22 ;
:: thesis: verum
end;
hence lmlt (p,B1) = lmlt (p,B2) by A1, A3, Lm1; :: thesis: verum