let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds (0. V1) |-- b1 = (len b1) |-> (0. K)
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 holds (0. V1) |-- b1 = (len b1) |-> (0. K)
let b1 be OrdBasis of V1; :: thesis: (0. V1) |-- b1 = (len b1) |-> (0. K)

per cases ( dom b1 = {} or dom b1 <> {} ) ;

suppose A1: dom b1 = {} ; :: thesis: (0. V1) |-- b1 = (len b1) |-> (0. K)

then A2: len b1 = 0 by CARD_1:47, RELAT_1:64;
len ((0. V1) |-- b1) = len b1 by MATRLIN:def 9;
hence (0. V1) |-- b1 = {} by A1, CARD_1:47, RELAT_1:64
.= (len b1) |-> (0. K) by A2 ;
:: thesis: verum

end;

suppose dom b1 <> {} ; :: thesis: (0. V1) |-- b1 = (len b1) |-> (0. K)

then consider x being set such that
A3: x in dom b1 by XBOOLE_0:def 1;
A4: width (1. K,(len b1)) = len b1 by MATRIX_1:25;
reconsider x = x as Nat by A3;
0. V1 = (b1 /. x) - (b1 /. x) by VECTSP_1:63
.= (b1 /. x) + ((- (1_ K)) * (b1 /. x)) by VECTSP_1:59 ;
hence (0. V1) |-- b1 = ((b1 /. x) |-- b1) + (((- (1_ K)) * (b1 /. x)) |-- b1) by Th17
.= ((b1 /. x) |-- b1) + ((- (1_ K)) * ((b1 /. x) |-- b1)) by Th18
.= (Line (1. K,(len b1)),x) + ((- (1_ K)) * ((b1 /. x) |-- b1)) by A3, Th19
.= (Line (1. K,(len b1)),x) + ((- (1_ K)) * (Line (1. K,(len b1)),x)) by A3, Th19
.= (Line (1. K,(len b1)),x) + (- (Line (1. K,(len b1)),x)) by FVSUM_1:72
.= (len b1) |-> (0. K) by A4, FVSUM_1:35 ;
:: thesis: verum

end;

end;