let n be Nat; :: thesis: for K being Field
for a being Element of K
for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let K be Field; :: thesis: for a being Element of K
for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let a be Element of K; :: thesis: for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let v, v1, v2 be Vector of (n -VectSp_over K); :: thesis: for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
let t, t1, t2 be Element of n -tuples_on the carrier of K; :: thesis: ( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
A1: addLoopStr(# the carrier of (n -VectSp_over K), the addF of (n -VectSp_over K), the ZeroF of (n -VectSp_over K) #) = n -Group_over K by PRVECT_1:def 5;
A2: n -Group_over K = addLoopStr(# (n -tuples_on the carrier of K),(product ( the addF of K,n)),(n |-> (0. K)) #) by PRVECT_1:def 3;
hence ( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) ) by A1; :: thesis: ( ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )
thus ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) by A2, A1, PRVECT_1:def 1; :: thesis: ( t = v implies a * t = a * v )
assume A3: t = v ; :: thesis: a * t = a * v
rng t c= the carrier of K by RELAT_1:def 19;
then A4: (id the carrier of K) * t = t by RELAT_1:53;
thus a * v = (n -Mult_over K) . (a,v) by PRVECT_1:def 5
.= the multF of K [;] (a,t) by A3, PRVECT_1:def 4
.= a * t by A4, FUNCOP_1:34 ; :: thesis: verum