set nV = n -VectSp_over K;
A1: now :: thesis: for v, u being Vector of (n -VectSp_over K) holds v + u = u + v
let v, u be Vector of (n -VectSp_over K); :: thesis: v + u = u + v
reconsider V = v, U = u as Element of n -tuples_on the carrier of K by Th102;
thus v + u = V + U by Th102
.= U + V by FINSEQOP:33
.= u + v by Th102 ; :: thesis: verum
end;
A2: now :: thesis: for v being Vector of (n -VectSp_over K) holds v + (0. (n -VectSp_over K)) = v
let v be Vector of (n -VectSp_over K); :: thesis: v + (0. (n -VectSp_over K)) = v
reconsider V = v, n0 = 0. (n -VectSp_over K) as Element of n -tuples_on the carrier of K by Th102;
thus v + (0. (n -VectSp_over K)) = V + n0 by Th102
.= V + (n |-> (0. K)) by Th102
.= v by FVSUM_1:21 ; :: thesis: verum
end;
A3: n -VectSp_over K is right_complementable
proof
reconsider N = n as Element of NAT by ORDINAL1:def 12;
let v be Vector of (n -VectSp_over K); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider V = v as Element of N -tuples_on the carrier of K by Th102;
reconsider u = - V as Element of (n -VectSp_over K) by Th102;
v + u = V + (- V) by Th102
.= n |-> (0. K) by FVSUM_1:26
.= 0. (n -VectSp_over K) by Th102 ;
hence ex u being Vector of (n -VectSp_over K) st v + u = 0. (n -VectSp_over K) ; :: according to ALGSTR_0:def 11 :: thesis: verum
end;
now :: thesis: for u, v, w being Vector of (n -VectSp_over K) holds (u + v) + w = u + (v + w)
let u, v, w be Vector of (n -VectSp_over K); :: thesis: (u + v) + w = u + (v + w)
reconsider V = v, U = u, W = w, UV = u + v, VW = v + w as Element of n -tuples_on the carrier of K by Th102;
thus (u + v) + w = UV + W by Th102
.= (U + V) + W by Th102
.= U + (V + W) by FINSEQOP:28
.= U + VW by Th102
.= u + (v + w) by Th102 ; :: thesis: verum
end;
hence ( n -VectSp_over K is right_complementable & n -VectSp_over K is Abelian & n -VectSp_over K is add-associative & n -VectSp_over K is right_zeroed ) by A2, A3, A1, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum