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:27, RELAT_1:41;
len ((0. V1) |-- b1) = len b1 by MATRLIN:def 7;
hence (0. V1) |-- b1 = {} by A1, CARD_1:27, RELAT_1:41
.= (len b1) |-> (0. K) by A2 ;
:: thesis: verum

end;

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

then consider x being object such that
A3: x in dom b1 by XBOOLE_0:def 1;
A4: width (1. (K,(len b1))) = len b1 by MATRIX_0:24;
reconsider x = x as Nat by A3;
0. V1 = (b1 /. x) - (b1 /. x) by VECTSP_1:16
.= (b1 /. x) + ((- (1_ K)) * (b1 /. x)) by VECTSP_1:14 ;
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:59
.= (len b1) |-> (0. K) by A4, FVSUM_1:26 ;
:: thesis: verum

end;

end;