set M = the lmult of V;
set W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #);
A1: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is vector-distributive
proof
let a be Element of GF; :: according to VECTSP_1:def 13 :: thesis: for b1, b2 being Element of the carrier of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds a * (b1 + b2) = (a * b1) + (a * b2)
let v, w be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider x = v, y = w as Element of V ;
thus a * (v + w) = a * (x + y)
.= (a * x) + (a * y) by VECTSP_1:def 14
.= (a * v) + (a * w) ; :: thesis: verum
end;
A2: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-distributive
proof
let a, b be Element of GF; :: according to VECTSP_1:def 14 :: thesis: for b1 being Element of the carrier of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds (a + b) * b1 = (a * b1) + (b * b1)
let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider x = v as Element of V ;
thus (a + b) * v = (a + b) * x
.= (a * x) + (b * x) by VECTSP_1:def 15
.= (a * v) + (b * v) ; :: thesis: verum
end;
A3: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-associative
proof
let a, b be Element of GF; :: according to VECTSP_1:def 15 :: thesis: for b1 being Element of the carrier of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds (a * b) * b1 = a * (b * b1)
let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a * b) * v = a * (b * v)
reconsider x = v as Element of V ;
thus (a * b) * v = (a * b) * x
.= a * (b * x) by VECTSP_1:def 16
.= a * (b * v) ; :: thesis: verum
end;
A4: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-unital
proof
let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to VECTSP_1:def 16 :: thesis: (1. GF) * v = v
reconsider x = v as Element of V ;
thus (1. GF) * v = (1_ GF) * x
.= v by VECTSP_1:def 17 ; :: thesis: verum
end;
A5: for a, b being Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
for x, y being Element of V st x = a & b = y holds
a + b = x + y ;
( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )
proof
thus ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian :: thesis: ( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )
proof
let a, b be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of V ;
thus a + b = y + x by A5
.= b + a ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )
let a, b, c be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of V ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable
let a be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: a + (0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = a
reconsider x = a as Element of V ;
thus a + (0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = x + (0. V)
.= a by RLVECT_1:4 ; :: thesis: verum
end;
let a be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of V ;
reconsider b = (comp V) . x as Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
thus a + b = x + (- x) by VECTSP_1:def 13
.= 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) by RLVECT_1:5 ; :: thesis: verum
end;
then reconsider W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF by A1, A2, A3, A4;
A6: ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19;
the lmult of W = the lmult of V | [: the carrier of GF, the carrier of W:] by RELSET_1:19;
then reconsider W = W as Subspace of V by A6, Def2;
take W ; :: thesis: W is strict
thus W is strict ; :: thesis: verum