:: VECTSP_1 semantic presentation

begin

definition
func G_Real  ->  strict addLoopStr  equals :: VECTSP_1:def 1
 addLoopStr(# REAL,addreal,0 #);
coherence
 addLoopStr(# REAL,addreal,0 #) is strict addLoopStr ;
end;

:: deftheorem  defines G_Real VECTSP_1:def_1_:_
 G_Real = addLoopStr(# REAL,addreal,0 #);

registration
cluster G_Real  ->  non empty strict ;
coherence
 not G_Real is empty ;
end;

registration
cluster the carrier of G_Real ->  real-membered ;
coherence
 the carrier of G_Real is real-membered ;
end;

registration
let a, b be Element of G_Real;
let x, y be real number ;
identifya + b with x + y when a = x, b = y;
compatibility
 ( a = x & b = y implies a + b = x + y ) by BINOP_2:def_9;
end;

registration
cluster G_Real  ->  strict right_complementable Abelian add-associative right_zeroed ;
coherence
 ( G_Real is Abelian & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )
proof
thus  for x, y being Element of G_Real holds x + y = y + x ; :: according to RLVECT_1:def_2 ::_thesis: ( G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )
thus  for x, y, z being Element of G_Real holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def_3 ::_thesis: ( G_Real is right_zeroed & G_Real is right_complementable )
thus  for x being Element of G_Real holds x + (0. G_Real) = x ; :: according to RLVECT_1:def_4 ::_thesis: G_Real is right_complementable
let x be Element of G_Real; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Element of REAL ;
reconsider y = - x9 as Element of G_Real ;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. G_Real
thus  x + y = 0. G_Real ; ::_thesis: verum
end;
end;

registration
let a be Element of G_Real;
let x be real number ;
identify - a with  - x when a = x;
compatibility
 ( a = x implies - a = - x )
proof
reconsider b = - x as Element of G_Real ;
assume  x = a ; ::_thesis: - a = - x
then  b + a = 0. G_Real ;
hence  - a = - x by RLVECT_1:6; ::_thesis: verum
end;
end;

theorem :: VECTSP_1:1
for x, y, z being Element of G_Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Real) = x & x + (- x) = 0. G_Real ) ;

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed for addLoopStr ;
existence
 ex b1 being non empty addLoopStr st
( b1 is strict & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian )
proof
take  G_Real ; ::_thesis: ( G_Real is strict & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable & G_Real is Abelian )
thus  ( G_Real is strict & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable & G_Real is Abelian ) ; ::_thesis: verum
end;
end;

definition
mode AddGroup is non empty right_complementable add-associative right_zeroed addLoopStr ;
end;

definition
mode AbGroup is Abelian AddGroup;
end;

definition
let IT be non empty doubleLoopStr ;
attrIT is right-distributive  means :Def2: :: VECTSP_1:def 2
 for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c);
attrIT is left-distributive  means :Def3: :: VECTSP_1:def 3
 for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a);
end;

:: deftheorem Def2 defines right-distributive VECTSP_1:def_2_:_
 for IT being non empty doubleLoopStr holds
( IT is right-distributive iff for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c) );

:: deftheorem Def3 defines left-distributive VECTSP_1:def_3_:_
 for IT being non empty doubleLoopStr holds
( IT is left-distributive iff for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a) );

definition
let IT be non empty multLoopStr ;
attrIT is right_unital  means :Def4: :: VECTSP_1:def 4
 for x being Element of IT holds x * (1. IT) = x;
end;

:: deftheorem Def4 defines right_unital VECTSP_1:def_4_:_
 for IT being non empty multLoopStr holds
( IT is right_unital iff for x being Element of IT holds x * (1. IT) = x );

definition
func F_Real  ->  strict doubleLoopStr  equals :: VECTSP_1:def 5
 doubleLoopStr(# REAL,addreal,multreal,1,0 #);
correctness
coherence
doubleLoopStr(# REAL,addreal,multreal,1,0 #) is strict doubleLoopStr ;
;
end;

:: deftheorem  defines F_Real VECTSP_1:def_5_:_
 F_Real = doubleLoopStr(# REAL,addreal,multreal,1,0 #);

registration
cluster F_Real  ->  non empty strict ;
coherence
 not F_Real is empty ;
end;

registration
cluster the carrier of F_Real ->  real-membered ;
coherence
 the carrier of F_Real is real-membered ;
end;

registration
let a, b be Element of F_Real;
let x, y be real number ;
identifya + b with x + y when a = x, b = y;
compatibility
 ( a = x & b = y implies a + b = x + y ) by BINOP_2:def_9;
end;

registration
let a, b be Element of F_Real;
let x, y be real number ;
identifya * b with x * y when a = x, b = y;
compatibility
 ( a = x & b = y implies a * b = x * y ) by BINOP_2:def_11;
end;

definition
let IT be non empty multLoopStr ;
attrIT is well-unital  means :Def6: :: VECTSP_1:def 6
 for x being Element of IT holds
( x * (1. IT) = x & (1. IT) * x = x );
end;

:: deftheorem Def6 defines well-unital VECTSP_1:def_6_:_
 for IT being non empty multLoopStr holds
( IT is well-unital iff for x being Element of IT holds
( x * (1. IT) = x & (1. IT) * x = x ) );

Lm1:  for L being non empty multLoopStr st L is well-unital holds
L is unital
proof
let L be non empty multLoopStr ; ::_thesis: ( L is well-unital implies L is unital )
assume A1: L is well-unital ; ::_thesis: L is unital
take  1. L ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of L holds
( b1 * (1. L) = b1 & (1. L) * b1 = b1 )
thus  for b1 being Element of the carrier of L holds
( b1 * (1. L) = b1 & (1. L) * b1 = b1 ) by A1, Def6; ::_thesis: verum
end;

Lm2:  for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L
proof
let L be non empty multLoopStr ; ::_thesis: ( L is well-unital implies 1. L = 1_ L )
assume  L is well-unital ; ::_thesis: 1. L = 1_ L
then  ( ( for h being Element of L holds
( h * (1. L) = h & (1. L) * h = h ) ) & L is unital ) by Def6, Lm1;
hence  1. L = 1_ L by GROUP_1:def_4; ::_thesis: verum
end;

registration
cluster F_Real  ->  strict well-unital ;
coherence
 F_Real is well-unital
proof
let x be Element of F_Real; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. F_Real) = x & (1. F_Real) * x = x )
thus  ( x * (1. F_Real) = x & (1. F_Real) * x = x ) ; ::_thesis: verum
end;
end;

registration
cluster non empty well-unital for multLoopStr_0 ;
existence
 ex b1 being non empty multLoopStr_0 st b1 is well-unital
proof
take  F_Real ; ::_thesis: F_Real is well-unital
thus  F_Real is well-unital ; ::_thesis: verum
end;
end;

definition
let IT be non empty doubleLoopStr ;
attrIT is distributive  means :Def7: :: VECTSP_1:def 7
 for x, y, z being Element of IT holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) );
end;

:: deftheorem Def7 defines distributive VECTSP_1:def_7_:_
 for IT being non empty doubleLoopStr holds
( IT is distributive iff for x, y, z being Element of IT holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) );

definition
let IT be non empty multLoopStr ;
attrIT is left_unital  means :Def8: :: VECTSP_1:def 8
 for x being Element of IT holds (1. IT) * x = x;
end;

:: deftheorem Def8 defines left_unital VECTSP_1:def_8_:_
 for IT being non empty multLoopStr holds
( IT is left_unital iff for x being Element of IT holds (1. IT) * x = x );

definition
let IT be non empty multLoopStr_0 ;
redefine attr IT is almost_left_invertible  means :Def9: :: VECTSP_1:def 9
 for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT;
compatibility
 ( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT )
proof
thus  ( IT is almost_left_invertible implies for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT ) ::_thesis: ( ( for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT ) implies IT is almost_left_invertible )
proof
assume A1: IT is almost_left_invertible ; ::_thesis: for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT
let x be Element of IT; ::_thesis: ( x <> 0. IT implies ex y being Element of IT st y * x = 1. IT )
assume  x <> 0. IT ; ::_thesis: ex y being Element of IT st y * x = 1. IT
then  x is left_invertible by A1, ALGSTR_0:def_39;
hence  ex y being Element of IT st y * x = 1. IT by ALGSTR_0:def_27; ::_thesis: verum
end;
assume A2: for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT ; ::_thesis: IT is almost_left_invertible
let x be Element of IT; :: according to ALGSTR_0:def_39 ::_thesis: ( x = 0. IT or x is left_invertible )
assume  x <> 0. IT ; ::_thesis: x is left_invertible
hence  ex y being Element of IT st y * x = 1. IT by A2; :: according to ALGSTR_0:def_27 ::_thesis: verum
end;
end;

:: deftheorem Def9 defines almost_left_invertible VECTSP_1:def_9_:_
 for IT being non empty multLoopStr_0 holds
( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT );

set FR = F_Real ;

registration
cluster F_Real  ->  strict unital ;
coherence
 F_Real is unital
proof
reconsider e = 1 as Element of F_Real ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of F_Real holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of F_Real holds
( b1 * e = b1 & e * b1 = b1 ) ; ::_thesis: verum
end;
end;

registration
cluster F_Real  ->  non degenerated right_complementable almost_left_invertible strict Abelian add-associative right_zeroed associative commutative right_unital distributive left_unital ;
coherence
 ( F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
proof
thus  for x, y, z being Element of F_Real holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def_3 ::_thesis: ( F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  for x being Element of F_Real holds x + (0. F_Real) = x ; :: according to RLVECT_1:def_4 ::_thesis: ( F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  F_Real is right_complementable ::_thesis: ( F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
proof
let x be Element of F_Real; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Element of REAL ;
reconsider y = - x9 as Element of F_Real ;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. F_Real
thus  x + y = 0. F_Real ; ::_thesis: verum
end;
thus  for x, y being Element of F_Real holds x + y = y + x ; :: according to RLVECT_1:def_2 ::_thesis: ( F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  for x, y being Element of F_Real holds x * y = y * x ; :: according to GROUP_1:def_12 ::_thesis: ( F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  for x, y, z being Element of F_Real holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def_3 ::_thesis: ( F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  for x being Element of F_Real holds (1. F_Real) * x = x ; :: according to VECTSP_1:def_8 ::_thesis: ( F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  for x being Element of F_Real holds x * (1. F_Real) = x ; :: according to VECTSP_1:def_4 ::_thesis: ( F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus  for x, y, z being Element of F_Real holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ; :: according to VECTSP_1:def_7 ::_thesis: ( F_Real is almost_left_invertible & not F_Real is degenerated )
hereby  :: according to VECTSP_1:def_9 ::_thesis: not F_Real is degenerated
let x be Element of F_Real; ::_thesis: ( x <> 0. F_Real implies ex y being Element of F_Real st y * x = 1. F_Real )
reconsider x9 = x as Element of REAL ;
assume A1: x <> 0. F_Real ; ::_thesis: ex y being Element of F_Real st y * x = 1. F_Real
reconsider y = x9 " as Element of F_Real ;
take y = y; ::_thesis: y * x = 1. F_Real
thus  y * x = 1. F_Real by A1, XCMPLX_0:def_7; ::_thesis: verum
end;
thus  0. F_Real <> 1. F_Real ; :: according to STRUCT_0:def_8 ::_thesis: verum
end;
end;

registration
let a be Element of F_Real;
let x be real number ;
identify - a with  - x when a = x;
compatibility
 ( a = x implies - a = - x )
proof
reconsider b = - x as Element of F_Real ;
assume  x = a ; ::_thesis: - a = - x
then  b + a = 0. F_Real ;
hence  - a = - x by RLVECT_1:6; ::_thesis: verum
end;
end;

Lm3:  for L being non empty doubleLoopStr st L is distributive holds
( L is right-distributive & L is left-distributive )
proof
let L be non empty doubleLoopStr ; ::_thesis: ( L is distributive implies ( L is right-distributive & L is left-distributive ) )
assume A1: L is distributive ; ::_thesis: ( L is right-distributive & L is left-distributive )
then  for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) by Def7;
hence  L is right-distributive by Def2; ::_thesis: L is left-distributive
 for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) by A1, Def7;
hence  L is left-distributive by Def3; ::_thesis: verum
end;

registration
cluster non empty distributive  ->  non empty right-distributive left-distributive for doubleLoopStr ;
coherence
 for b1 being non empty doubleLoopStr st b1 is distributive holds
( b1 is left-distributive & b1 is right-distributive ) by Lm3;
cluster non empty right-distributive left-distributive  ->  non empty distributive for doubleLoopStr ;
coherence
 for b1 being non empty doubleLoopStr st b1 is left-distributive & b1 is right-distributive holds
b1 is distributive
proof
let D be non empty doubleLoopStr ; ::_thesis: ( D is left-distributive & D is right-distributive implies D is distributive )
assume  ( ( for a, b, c being Element of D holds (b + c) * a = (b * a) + (c * a) ) & ( for a, b, c being Element of D holds a * (b + c) = (a * b) + (a * c) ) ) ; :: according to VECTSP_1:def_2,VECTSP_1:def_3 ::_thesis: D is distributive
hence  for x, y, z being Element of D holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ; :: according to VECTSP_1:def_7 ::_thesis: verum
end;
end;

registration
cluster non empty well-unital  ->  non empty right_unital left_unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is well-unital holds
( b1 is left_unital & b1 is right_unital )
proof
let L be non empty multLoopStr ; ::_thesis: ( L is well-unital implies ( L is left_unital & L is right_unital ) )
assume A1: L is well-unital ; ::_thesis: ( L is left_unital & L is right_unital )
hence  for x being Element of L holds (1. L) * x = x by Def6; :: according to VECTSP_1:def_8 ::_thesis: L is right_unital
thus  for x being Element of L holds x * (1. L) = x by A1, Def6; :: according to VECTSP_1:def_4 ::_thesis: verum
end;
cluster non empty right_unital left_unital  ->  non empty unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is left_unital & b1 is right_unital holds
b1 is unital
proof
let L be non empty multLoopStr ; ::_thesis: ( L is left_unital & L is right_unital implies L is unital )
assume A2: ( ( for x being Element of L holds (1. L) * x = x ) & ( for x being Element of L holds x * (1. L) = x ) ) ; :: according to VECTSP_1:def_4,VECTSP_1:def_8 ::_thesis: L is unital
take  1. L ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of L holds
( b1 * (1. L) = b1 & (1. L) * b1 = b1 )
thus  for b1 being Element of the carrier of L holds
( b1 * (1. L) = b1 & (1. L) * b1 = b1 ) by A2; ::_thesis: verum
end;
end;

registration
cluster non empty associative commutative for multMagma ;
existence
 ex b1 being non empty multMagma st
( b1 is commutative & b1 is associative )
proof
take  F_Real ; ::_thesis: ( F_Real is commutative & F_Real is associative )
thus  ( F_Real is commutative & F_Real is associative ) ; ::_thesis: verum
end;
end;

registration
cluster non empty unital associative commutative for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st
( b1 is commutative & b1 is associative & b1 is unital )
proof
take  F_Real ; ::_thesis: ( F_Real is commutative & F_Real is associative & F_Real is unital )
thus  ( F_Real is commutative & F_Real is associative & F_Real is unital ) ; ::_thesis: verum
end;
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible strict Abelian add-associative right_zeroed associative commutative right_unital well-unital distributive left_unital for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is left_unital & b1 is right_unital & b1 is distributive & b1 is almost_left_invertible & not b1 is degenerated & b1 is well-unital & b1 is strict )
proof
take  F_Real ; ::_thesis: ( F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated & F_Real is well-unital & F_Real is strict )
thus  ( F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated & F_Real is well-unital & F_Real is strict ) ; ::_thesis: verum
end;
end;

definition
mode Field is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
end;

theorem :: VECTSP_1:2
1. F_Real = 1 ;

theorem :: VECTSP_1:3
for x, y, z being Element of F_Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F_Real) = x & x + (- x) = 0. F_Real & x * y = y * x & (x * y) * z = x * (y * z) & (1. F_Real) * x = x & ( x <> 0. F_Real implies ex y being Element of F_Real st y * x = 1. F_Real ) & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Def9;

theorem :: VECTSP_1:4
for FS being non empty doubleLoopStr holds
( ( for x, y, z being Element of FS holds
( ( x <> 0. FS implies ex y being Element of FS st y * x = 1. FS ) & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ) iff FS is non empty almost_left_invertible distributive doubleLoopStr ) by Def7, Def9;

registration
cluster non empty well-unital  ->  non empty unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is well-unital holds
b1 is unital ;
end;

theorem :: VECTSP_1:5
for F being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x, y, z being Element of F st x <> 0. F & x * y = x * z holds
y = z
proof
let F be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x, y, z being Element of F st x <> 0. F & x * y = x * z holds
y = z
let x, y, z be Element of F; ::_thesis: ( x <> 0. F & x * y = x * z implies y = z )
assume  x <> 0. F ; ::_thesis: ( not x * y = x * z or y = z )
then consider x1 being Element of F such that
A1: x1 * x = 1. F by Def9;
A2: ( (x1 * x) * y = x1 * (x * y) & x1 * (x * z) = (x1 * x) * z ) by GROUP_1:def_3;
assume  x * y = x * z ; ::_thesis: y = z
then  (x * x1) * y = z by A1, A2, Def8;
hence  y = z by A1, Def8; ::_thesis: verum
end;

definition
let F be non empty almost_left_invertible associative commutative well-unital doubleLoopStr ;
let x be Element of F;
assume A1: x <> 0. F ;
redefine func x "  means :Def10: :: VECTSP_1:def 10
it * x = 1. F;
compatibility
 for b1 being Element of the carrier of F holds
( b1 = x " iff b1 * x = 1. F )
proof
let IT be Element of F; ::_thesis: ( IT = x " iff IT * x = 1. F )
A2: x is left_invertible by A1, ALGSTR_0:def_39;
then consider x1 being Element of F such that
A3: x1 * x = 1. F by ALGSTR_0:def_27;
 x is right_mult-cancelable
proof
let y, z be Element of F; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z )
assume A4: y * x = z * x ; ::_thesis: y = z
thus y = y * (1. F) by Def6
.= (z * x) * x1 by A3, A4, GROUP_1:def_3
.= z * (1. F) by A3, GROUP_1:def_3
.= z by Def6 ; ::_thesis: verum
end;
hence  ( IT = x " iff IT * x = 1. F ) by A2, ALGSTR_0:def_35; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines " VECTSP_1:def_10_:_
 for F being non empty almost_left_invertible associative commutative well-unital doubleLoopStr
for x being Element of F st x <> 0. F holds
for b3 being Element of the carrier of F holds
( b3 = x " iff b3 * x = 1. F );

definition
let F be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let x, y be Element of F;
funcx / y ->  Element of F equals :: VECTSP_1:def 11
x * (y ");
coherence
 x * (y ") is Element of F ;
end;

:: deftheorem  defines / VECTSP_1:def_11_:_
 for F being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x, y being Element of F holds x / y = x * (y ");

theorem Th6: :: VECTSP_1:6
for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for x being Element of F holds x * (0. F) = 0. F
proof
let F be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for x being Element of F holds x * (0. F) = 0. F
let x be Element of F; ::_thesis: x * (0. F) = 0. F
(x * (0. F)) + (0. F) = (x * ((0. F) + (0. F))) + (0. F) by RLVECT_1:4
.= x * ((0. F) + (0. F)) by RLVECT_1:4
.= (x * (0. F)) + (x * (0. F)) by Def2 ;
hence  x * (0. F) = 0. F by RLVECT_1:8; ::_thesis: verum
end;

theorem Th7: :: VECTSP_1:7
for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x being Element of F holds (0. F) * x = 0. F
proof
let F be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for x being Element of F holds (0. F) * x = 0. F
let x be Element of F; ::_thesis: (0. F) * x = 0. F
((0. F) * x) + (0. F) = (((0. F) + (0. F)) * x) + (0. F) by RLVECT_1:4
.= ((0. F) + (0. F)) * x by RLVECT_1:4
.= ((0. F) * x) + ((0. F) * x) by Def3 ;
hence  (0. F) * x = 0. F by RLVECT_1:8; ::_thesis: verum
end;

theorem Th8: :: VECTSP_1:8
for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for x, y being Element of F holds x * (- y) = - (x * y)
proof
let F be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for x, y being Element of F holds x * (- y) = - (x * y)
let x, y be Element of F; ::_thesis: x * (- y) = - (x * y)
(x * y) + (x * (- y)) = x * (y + (- y)) by Def2
.= x * (0. F) by RLVECT_1:def_10
.= 0. F by Th6 ;
hence  x * (- y) = - (x * y) by RLVECT_1:def_10; ::_thesis: verum
end;

theorem Th9: :: VECTSP_1:9
for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x, y being Element of F holds (- x) * y = - (x * y)
proof
let F be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for x, y being Element of F holds (- x) * y = - (x * y)
let x, y be Element of F; ::_thesis: (- x) * y = - (x * y)
(x * y) + ((- x) * y) = (x + (- x)) * y by Def3
.= (0. F) * y by RLVECT_1:def_10
.= 0. F by Th7 ;
hence  (- x) * y = - (x * y) by RLVECT_1:def_10; ::_thesis: verum
end;

theorem Th10: :: VECTSP_1:10
for F being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x, y being Element of F holds (- x) * (- y) = x * y
proof
let F be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for x, y being Element of F holds (- x) * (- y) = x * y
let x, y be Element of F; ::_thesis: (- x) * (- y) = x * y
thus (- x) * (- y) = - (x * (- y)) by Th9
.= - (- (x * y)) by Th8
.= x * y by RLVECT_1:17 ; ::_thesis: verum
end;

theorem :: VECTSP_1:11
for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)
proof
let F be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)
let x, y, z be Element of F; ::_thesis: x * (y - z) = (x * y) - (x * z)
x * (y - z) = (x * y) + (x * (- z)) by Def2
.= (x * y) - (x * z) by Th8 ;
hence  x * (y - z) = (x * y) - (x * z) ; ::_thesis: verum
end;

theorem Th12: :: VECTSP_1:12
for F being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for x, y being Element of F holds
( x * y = 0. F iff ( x = 0. F or y = 0. F ) )
proof
let F be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x, y being Element of F holds
( x * y = 0. F iff ( x = 0. F or y = 0. F ) )
let x, y be Element of F; ::_thesis: ( x * y = 0. F iff ( x = 0. F or y = 0. F ) )
 ( not x * y = 0. F or x = 0. F or y = 0. F )
proof
assume A1: x * y = 0. F ; ::_thesis: ( x = 0. F or y = 0. F )
assume A2: x <> 0. F ; ::_thesis: y = 0. F
(x ") * (0. F) = ((x ") * x) * y by A1, GROUP_1:def_3
.= (1. F) * y by A2, Def10
.= y by Def8 ;
hence  y = 0. F by Th7; ::_thesis: verum
end;
hence  ( x * y = 0. F iff ( x = 0. F or y = 0. F ) ) by Th7; ::_thesis: verum
end;

theorem :: VECTSP_1:13
for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)
proof
let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)
let y, z, x be Element of K; ::_thesis: (y - z) * x = (y * x) - (z * x)
thus (y - z) * x = (y * x) + ((- z) * x) by Def3
.= (y * x) - (z * x) by Th9 ; ::_thesis: verum
end;

definition
let F be 1-sorted ;
attrc2 is strict ;
struct VectSpStr over F ->  addLoopStr ;
aggrVectSpStr(# carrier, addF, ZeroF, lmult #) ->  VectSpStr over F;
sel lmult c2 ->  Function of [: the carrier of F, the carrier of c2:], the carrier of c2;
end;

registration
let F be 1-sorted ;
cluster non empty strict for VectSpStr over F;
existence
 ex b1 being VectSpStr over F st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set a = the BinOp of the non empty set ;
set Z = the Element of the non empty set ;
set l = the Function of [: the carrier of F, the non empty set :], the non empty set ;
take  VectSpStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set #) ; ::_thesis: ( not VectSpStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set #) is empty & VectSpStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set #) is strict )
thus  not the carrier of VectSpStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: VectSpStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set #) is strict
thus  VectSpStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set #) is strict ; ::_thesis: verum
end;
end;

registration
let F be 1-sorted ;
let A be non empty set ;
let a be BinOp of A;
let Z be Element of A;
let l be Function of [: the carrier of F,A:],A;
cluster VectSpStr(# A,a,Z,l #) ->  non empty ;
coherence
 not VectSpStr(# A,a,Z,l #) is empty ;
end;

definition
let F be 1-sorted ;
mode Scalar of F is Element of F;
end;

definition
let F be 1-sorted ;
let VS be VectSpStr over F;
mode Scalar of VS is Scalar of F;
mode Vector of VS is Element of VS;
end;

definition
let F be non empty 1-sorted ;
let V be non empty VectSpStr over F;
let x be Element of F;
let v be Element of V;
funcx * v ->  Element of V equals :: VECTSP_1:def 12
 the lmult of V . (x,v);
coherence
 the lmult of V . (x,v) is Element of V ;
end;

:: deftheorem  defines * VECTSP_1:def_12_:_
 for F being non empty 1-sorted
for V being non empty VectSpStr over F
for x being Element of F
for v being Element of V holds x * v = the lmult of V . (x,v);

definition
let F be non empty addLoopStr ;
func comp F ->  UnOp of the carrier of F means :: VECTSP_1:def 13
 for x being Element of F holds it . x = - x;
existence
 ex b1 being UnOp of the carrier of F st
for x being Element of F holds b1 . x = - x
proof
deffunc H1( Element of F) ->  Element of the carrier of F = - $1;
thus  ex f being UnOp of the carrier of F st
for x being Element of F holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of the carrier of F st ( for x being Element of F holds b1 . x = - x ) & ( for x being Element of F holds b2 . x = - x ) holds
b1 = b2
proof
let f, g be UnOp of the carrier of F; ::_thesis: ( ( for x being Element of F holds f . x = - x ) & ( for x being Element of F holds g . x = - x ) implies f = g )
assume that
A1: for x being Element of F holds f . x = - x and
A2: for x being Element of F holds g . x = - x ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_F_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of F implies f . x = g . x )
assume  x in the carrier of F ; ::_thesis: f . x = g . x
then reconsider y = x as Element of F ;
thus f . x = - y by A1
.= g . x by A2 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem  defines comp VECTSP_1:def_13_:_
 for F being non empty addLoopStr
for b2 being UnOp of the carrier of F holds
( b2 = comp F iff for x being Element of F holds b2 . x = - x );

Lm4: now__::_thesis:_for_F_being_non_empty_right_complementable_Abelian_add-associative_right_zeroed_associative_distributive_left_unital_doubleLoopStr_
for_MLT_being_Function_of_[:_the_carrier_of_F,_the_carrier_of_F:],_the_carrier_of_F_holds_
(_VectSpStr(#_the_carrier_of_F,_the_addF_of_F,(0._F),MLT_#)_is_Abelian_&_VectSpStr(#_the_carrier_of_F,_the_addF_of_F,(0._F),MLT_#)_is_add-associative_&_VectSpStr(#_the_carrier_of_F,_the_addF_of_F,(0._F),MLT_#)_is_right_zeroed_&_VectSpStr(#_the_carrier_of_F,_the_addF_of_F,(0._F),MLT_#)_is_right_complementable_)
let F be non empty right_complementable Abelian add-associative right_zeroed associative distributive left_unital doubleLoopStr ; ::_thesis: for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F holds
( VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )
let MLT be Function of [: the carrier of F, the carrier of F:], the carrier of F; ::_thesis: ( VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )
set GF = VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #);
thus  VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian ::_thesis: ( VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )
proof
let x, y be Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider x9 = x, y9 = y as Element of F ;
thus x + y = y9 + x9 by RLVECT_1:2
.= y + x ; ::_thesis: verum
end;
thus  VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative ::_thesis: ( VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )
proof
let x, y, z be Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Element of F ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: verum
end;
thus  VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed ::_thesis: VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable
proof
let x be Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to RLVECT_1:def_4 ::_thesis: x + (0. VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #)) = x
reconsider x9 = x as Element of F ;
thus x + (0. VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #)) = x9 + (0. F)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
thus  VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable ::_thesis: verum
proof
let x be Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Element of F ;
consider t being Element of F such that
A1: x9 + t = 0. F by ALGSTR_0:def_11;
reconsider t9 = t as Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) ;
take  t9 ; :: according to ALGSTR_0:def_11 ::_thesis: x + t9 = 0. VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #)
thus  x + t9 = 0. VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) by A1; ::_thesis: verum
end;
end;

Lm5: now__::_thesis:_for_F_being_non_empty_right_complementable_add-associative_right_zeroed_associative_well-unital_distributive_doubleLoopStr_
for_MLT_being_Function_of_[:_the_carrier_of_F,_the_carrier_of_F:],_the_carrier_of_F_st_MLT_=_the_multF_of_F_holds_
for_x,_y_being_Element_of_F
for_v,_w_being_Element_of_VectSpStr(#_the_carrier_of_F,_the_addF_of_F,(0._F),MLT_#)_holds_
(_x_*_(v_+_w)_=_(x_*_v)_+_(x_*_w)_&_(x_+_y)_*_v_=_(x_*_v)_+_(y_*_v)_&_(x_*_y)_*_v_=_x_*_(y_*_v)_&_(1._F)_*_v_=_v_)
let F be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F st MLT = the multF of F holds
for x, y being Element of F
for v, w being Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
let MLT be Function of [: the carrier of F, the carrier of F:], the carrier of F; ::_thesis: ( MLT = the multF of F implies for x, y being Element of F
for v, w being Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v ) )
assume A1: MLT = the multF of F ; ::_thesis: for x, y being Element of F
for v, w being Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
let x, y be Element of F; ::_thesis: for v, w being Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
set LS = VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #);
let v, w be Element of VectSpStr(# the carrier of F, the addF of F,(0. F),MLT #); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
reconsider v9 = v, w9 = w as Element of F ;
thus x * (v + w) = x * (v9 + w9) by A1
.= (x * v9) + (x * w9) by Def7
.= (x * v) + (x * w) by A1 ; ::_thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )
thus (x + y) * v = (x + y) * v9 by A1
.= (x * v9) + (y * v9) by Def7
.= (x * v) + (y * v) by A1 ; ::_thesis: ( (x * y) * v = x * (y * v) & (1. F) * v = v )
thus (x * y) * v = (x * y) * v9 by A1
.= x * (y * v9) by GROUP_1:def_3
.= x * (y * v) by A1 ; ::_thesis: (1. F) * v = v
thus (1. F) * v = (1. F) * v9 by A1
.= v by Def8 ; ::_thesis: verum
end;

definition
let F be non empty doubleLoopStr ;
let IT be non empty VectSpStr over F;
attrIT is vector-distributive  means :Def14: :: VECTSP_1:def 14
 for x being Element of F
for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w);
attrIT is scalar-distributive  means :Def15: :: VECTSP_1:def 15
 for x, y being Element of F
for v being Element of IT holds (x + y) * v = (x * v) + (y * v);
attrIT is scalar-associative  means :Def16: :: VECTSP_1:def 16
 for x, y being Element of F
for v being Element of IT holds (x * y) * v = x * (y * v);
attrIT is scalar-unital  means :Def17: :: VECTSP_1:def 17
 for v being Element of IT holds (1. F) * v = v;
end;

:: deftheorem Def14 defines vector-distributive VECTSP_1:def_14_:_
 for F being non empty doubleLoopStr
for IT being non empty VectSpStr over F holds
( IT is vector-distributive iff for x being Element of F
for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w) );

:: deftheorem Def15 defines scalar-distributive VECTSP_1:def_15_:_
 for F being non empty doubleLoopStr
for IT being non empty VectSpStr over F holds
( IT is scalar-distributive iff for x, y being Element of F
for v being Element of IT holds (x + y) * v = (x * v) + (y * v) );

:: deftheorem Def16 defines scalar-associative VECTSP_1:def_16_:_
 for F being non empty doubleLoopStr
for IT being non empty VectSpStr over F holds
( IT is scalar-associative iff for x, y being Element of F
for v being Element of IT holds (x * y) * v = x * (y * v) );

:: deftheorem Def17 defines scalar-unital VECTSP_1:def_17_:_
 for F being non empty doubleLoopStr
for IT being non empty VectSpStr over F holds
( IT is scalar-unital iff for v being Element of IT holds (1. F) * v = v );

registration
let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
cluster non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for VectSpStr over F;
existence
 ex b1 being non empty VectSpStr over F st
( b1 is scalar-distributive & b1 is vector-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is strict )
proof
take V = VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #); ::_thesis: ( V is scalar-distributive & V is vector-distributive & V is scalar-associative & V is scalar-unital & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus  for x, y being Element of F
for v being Element of V holds (x + y) * v = (x * v) + (y * v) by Lm5; :: according to VECTSP_1:def_15 ::_thesis: ( V is vector-distributive & V is scalar-associative & V is scalar-unital & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus  for x being Element of F
for v, w being Element of V holds x * (v + w) = (x * v) + (x * w) by Lm5; :: according to VECTSP_1:def_14 ::_thesis: ( V is scalar-associative & V is scalar-unital & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus  for x, y being Element of F
for v being Element of V holds (x * y) * v = x * (y * v) by Lm5; :: according to VECTSP_1:def_16 ::_thesis: ( V is scalar-unital & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus  for v being Element of V holds (1. F) * v = v by Lm5; :: according to VECTSP_1:def_17 ::_thesis: ( V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus  ( V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict ) by Lm4; ::_thesis: verum
end;
end;

definition
let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
mode VectSp of F is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F;
end;


theorem Th14: :: VECTSP_1:14
for F being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for x being Element of F
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
proof
let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of F
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
let x be Element of F; ::_thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
let v be Element of V; ::_thesis: ( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
v + ((0. F) * v) = ((1. F) * v) + ((0. F) * v) by Def17
.= ((1. F) + (0. F)) * v by Def15
.= (1. F) * v by RLVECT_1:4
.= v by Def17
.= v + (0. V) by RLVECT_1:4 ;
hence A1: (0. F) * v = 0. V by RLVECT_1:8; ::_thesis: ( (- (1. F)) * v = - v & x * (0. V) = 0. V )
((- (1. F)) * v) + v = ((- (1. F)) * v) + ((1. F) * v) by Def17
.= ((1. F) + (- (1. F))) * v by Def15
.= 0. V by A1, RLVECT_1:def_10 ;
then  ((- (1. F)) * v) + (v + (- v)) = (0. V) + (- v) by RLVECT_1:def_3;
then (0. V) + (- v) = ((- (1. F)) * v) + (0. V) by RLVECT_1:5
.= (- (1. F)) * v by RLVECT_1:4 ;
hence  (- (1. F)) * v = - v by RLVECT_1:4; ::_thesis: x * (0. V) = 0. V
x * (0. V) = (x * (0. F)) * v by A1, Def16
.= 0. V by A1, Th6 ;
hence  x * (0. V) = 0. V ; ::_thesis: verum
end;

theorem :: VECTSP_1:15
for F being Field
for x being Element of F
for V being VectSp of F
for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
proof
let F be Field; ::_thesis: for x being Element of F
for V being VectSp of F
for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let x be Element of F; ::_thesis: for V being VectSp of F
for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let V be VectSp of F; ::_thesis: for v being Element of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
let v be Element of V; ::_thesis: ( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
 ( not x * v = 0. V or x = 0. F or v = 0. V )
proof
assume  x * v = 0. V ; ::_thesis: ( x = 0. F or v = 0. V )
then A1: ((x ") * x) * v = (x ") * (0. V) by Def16
.= 0. V by Th14 ;
assume  x <> 0. F ; ::_thesis: v = 0. V
then  0. V = (1. F) * v by A1, Def10;
hence  v = 0. V by Def17; ::_thesis: verum
end;
hence  ( x * v = 0. V iff ( x = 0. F or v = 0. V ) ) by Th14; ::_thesis: verum
end;

theorem :: VECTSP_1:16
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds
( v + w = 0. V iff - v = w )
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds
( v + w = 0. V iff - v = w )
let v, w be Element of V; ::_thesis: ( v + w = 0. V iff - v = w )
 ( v + w = 0. V implies - v = w )
proof
assume A1: v + w = 0. V ; ::_thesis: - v = w
thus w = (0. V) + w by RLVECT_1:4
.= ((- v) + v) + w by RLVECT_1:5
.= (- v) + (0. V) by A1, RLVECT_1:def_3
.= - v by RLVECT_1:4 ; ::_thesis: verum
end;
hence  ( v + w = 0. V iff - v = w ) by RLVECT_1:5; ::_thesis: verum
end;

Lm6:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (w + (- v)) = v - w
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds - (w + (- v)) = v - w
let v, w be Element of V; ::_thesis: - (w + (- v)) = v - w
 - (w + (- v)) = (- (- v)) - w by RLVECT_1:30;
hence  - (w + (- v)) = v - w by RLVECT_1:17; ::_thesis: verum
end;

Lm7:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - ((- v) - w) = w + v
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of V holds - ((- v) - w) = w + v
let v, w be Element of V; ::_thesis: - ((- v) - w) = w + v
 - ((- v) - w) = w + (- (- v)) by RLVECT_1:33;
hence  - ((- v) - w) = w + v by RLVECT_1:17; ::_thesis: verum
end;

theorem :: VECTSP_1:17
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v, w being Element of V holds
( - (v + w) = (- w) - v & - (w + (- v)) = v - w & - (v - w) = w + (- v) & - ((- v) - w) = w + v & u - (w + v) = (u - v) - w ) by Lm6, Lm7, RLVECT_1:27, RLVECT_1:30, RLVECT_1:33;

theorem :: VECTSP_1:18
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( (0. V) - v = - v & v - (0. V) = v ) by RLVECT_1:13, RLVECT_1:14;

theorem Th19: :: VECTSP_1:19
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for x, y being Element of F holds
( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for x, y being Element of F holds
( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
let x, y be Element of F; ::_thesis: ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
 ( x + (- y) = 0. F implies x = y )
proof
assume  x + (- y) = 0. F ; ::_thesis: x = y
then  x + ((- y) + y) = (0. F) + y by RLVECT_1:def_3;
then  x + (0. F) = (0. F) + y by RLVECT_1:5;
then  x = (0. F) + y by RLVECT_1:4;
hence  x = y by RLVECT_1:4; ::_thesis: verum
end;
hence  ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) ) by RLVECT_1:5; ::_thesis: verum
end;

theorem :: VECTSP_1:20
for F being Field
for x being Element of F
for V being VectSp of F
for v being Element of V st x <> 0. F holds
(x ") * (x * v) = v
proof
let F be Field; ::_thesis: for x being Element of F
for V being VectSp of F
for v being Element of V st x <> 0. F holds
(x ") * (x * v) = v
let x be Element of F; ::_thesis: for V being VectSp of F
for v being Element of V st x <> 0. F holds
(x ") * (x * v) = v
let V be VectSp of F; ::_thesis: for v being Element of V st x <> 0. F holds
(x ") * (x * v) = v
let v be Element of V; ::_thesis: ( x <> 0. F implies (x ") * (x * v) = v )
assume A1: x <> 0. F ; ::_thesis: (x ") * (x * v) = v
(x ") * (x * v) = ((x ") * x) * v by Def16
.= (1. F) * v by A1, Def10
.= v by Def17 ;
hence  (x ") * (x * v) = v ; ::_thesis: verum
end;

theorem Th21: :: VECTSP_1:21
for F being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for x being Element of F
for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
proof
let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for x being Element of F
for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for x being Element of F
for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
let x be Element of F; ::_thesis: for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
let v, w be Element of V; ::_thesis: ( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
A1: - (x * v) = (- (1. F)) * (x * v) by Th14
.= ((- (1. F)) * x) * v by Def16
.= (- ((1. F) * x)) * v by Th9 ;
hence  - (x * v) = (- x) * v by Def8; ::_thesis: w - (x * v) = w + ((- x) * v)
thus  w - (x * v) = w + ((- x) * v) by A1, Def8; ::_thesis: verum
end;

registration
cluster non empty commutative left_unital  ->  non empty right_unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is commutative & b1 is left_unital holds
b1 is right_unital
proof
let F be non empty multLoopStr ; ::_thesis: ( F is commutative & F is left_unital implies F is right_unital )
assume A1: ( F is commutative & F is left_unital ) ; ::_thesis: F is right_unital
let x be Scalar of F; :: according to VECTSP_1:def_4 ::_thesis: x * (1. F) = x
 for F being non empty commutative multMagma
for x, y being Element of F holds x * y = y * x ;
then  x * (1. F) = (1. F) * x by A1;
hence  x * (1. F) = x by A1, Def8; ::_thesis: verum
end;
end;

theorem Th22: :: VECTSP_1:22
for F being non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for x being Element of F
for v being Element of V holds x * (- v) = - (x * v)
proof
let F be non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for x being Element of F
for v being Element of V holds x * (- v) = - (x * v)
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for x being Element of F
for v being Element of V holds x * (- v) = - (x * v)
let x be Element of F; ::_thesis: for v being Element of V holds x * (- v) = - (x * v)
let v be Element of V; ::_thesis: x * (- v) = - (x * v)
x * (- v) = x * ((- (1. F)) * v) by Th14
.= (x * (- (1. F))) * v by Def16
.= (- (x * (1. F))) * v by Th8
.= (- x) * v by Def4 ;
hence  x * (- v) = - (x * v) by Th21; ::_thesis: verum
end;

theorem :: VECTSP_1:23
for F being non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for x being Element of F
for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)
proof
let F be non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for x being Element of F
for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for x being Element of F
for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)
let x be Element of F; ::_thesis: for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)
let v, w be Element of V; ::_thesis: x * (v - w) = (x * v) - (x * w)
x * (v - w) = (x * v) + (x * (- w)) by Def14
.= (x * v) + (- (x * w)) by Th22 ;
hence  x * (v - w) = (x * v) - (x * w) ; ::_thesis: verum
end;

theorem :: VECTSP_1:24
for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for x being Element of F st x <> 0. F holds
(x ") " = x
proof
let F be non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of F st x <> 0. F holds
(x ") " = x
let x be Element of F; ::_thesis: ( x <> 0. F implies (x ") " = x )
assume A1: x <> 0. F ; ::_thesis: (x ") " = x
 ( x <> 0. F implies x " <> 0. F )
proof
assume A2: x <> 0. F ; ::_thesis: x " <> 0. F
assume  not x " <> 0. F ; ::_thesis: contradiction
then  1. F = x * (0. F) by A2, Def10;
hence  contradiction by Th7; ::_thesis: verum
end;
then  (x ") * ((x ") ") = 1. F by A1, Def10;
then  (x * (x ")) * ((x ") ") = x * (1. F) by GROUP_1:def_3;
then  (1. F) * ((x ") ") = x * (1. F) by A1, Def10;
then  (x ") " = x * (1. F) by Def6;
hence  (x ") " = x by Def6; ::_thesis: verum
end;

theorem :: VECTSP_1:25
for F being Field
for x being Element of F st x <> 0. F holds
( x " <> 0. F & - (x ") <> 0. F )
proof
let F be Field; ::_thesis: for x being Element of F st x <> 0. F holds
( x " <> 0. F & - (x ") <> 0. F )
let x be Element of F; ::_thesis: ( x <> 0. F implies ( x " <> 0. F & - (x ") <> 0. F ) )
assume A1: x <> 0. F ; ::_thesis: ( x " <> 0. F & - (x ") <> 0. F )
hereby  ::_thesis: - (x ") <> 0. F
assume  x " = 0. F ; ::_thesis: contradiction
then  1. F = x * (0. F) by A1, Def10;
hence  contradiction by Th7; ::_thesis: verum
end;
assume  - (x ") = 0. F ; ::_thesis: contradiction
then  (1. F) * (x ") = (- (1. F)) * (0. F) by Th10;
then  (1. F) * (x ") = 0. F by Th7;
then  x * (x ") = x * (0. F) by Def8;
then  1. F = x * (0. F) by A1, Def10;
hence  contradiction by Th7; ::_thesis: verum
end;

theorem Th26: :: VECTSP_1:26
(1. F_Real) + (1. F_Real) <> 0. F_Real ;

definition
let IT be non empty addLoopStr ;
attrIT is Fanoian  means :Def18: :: VECTSP_1:def 18
 for a being Element of IT st a + a = 0. IT holds
a = 0. IT;
end;

:: deftheorem Def18 defines Fanoian VECTSP_1:def_18_:_
 for IT being non empty addLoopStr holds
( IT is Fanoian iff for a being Element of IT st a + a = 0. IT holds
a = 0. IT );

registration
cluster non empty Fanoian for addLoopStr ;
existence
 ex b1 being non empty addLoopStr st b1 is Fanoian
proof
take F = F_Real ; ::_thesis: F is Fanoian
let a be Element of F; :: according to VECTSP_1:def_18 ::_thesis: ( a + a = 0. F implies a = 0. F )
assume A1: a + a = 0. F ; ::_thesis: a = 0. F
 a = (1. F) * a by Def8;
then  a + a = ((1. F) + (1. F)) * a by Def7;
hence  a = 0. F by A1, Th12, Th26; ::_thesis: verum
end;
end;

definition
let F be non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
redefine attr F is Fanoian  means :Def19: :: VECTSP_1:def 19
(1. F) + (1. F) <> 0. F;
compatibility
 ( F is Fanoian iff (1. F) + (1. F) <> 0. F )
proof
thus  ( F is Fanoian implies (1. F) + (1. F) <> 0. F ) by Def18; ::_thesis: ( (1. F) + (1. F) <> 0. F implies F is Fanoian )
assume A1: (1. F) + (1. F) <> 0. F ; ::_thesis: F is Fanoian
let a be Element of F; :: according to VECTSP_1:def_18 ::_thesis: ( a + a = 0. F implies a = 0. F )
assume A2: a + a = 0. F ; ::_thesis: a = 0. F
 a = (1. F) * a by Def8;
then  a + a = ((1. F) + (1. F)) * a by Def7;
hence  a = 0. F by A1, A2, Th12; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines Fanoian VECTSP_1:def_19_:_
 for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds
( F is Fanoian iff (1. F) + (1. F) <> 0. F );

registration
cluster non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Fanoian for doubleLoopStr ;
existence
 ex b1 being Field st
( b1 is strict & b1 is Fanoian )
proof
 F_Real is Fanoian by Def19, Th26;
hence  ex b1 being Field st
( b1 is strict & b1 is Fanoian ) ; ::_thesis: verum
end;
end;

theorem :: VECTSP_1:27
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F st a - b = 0. F holds
a = b by Th19;

theorem Th28: :: VECTSP_1:28
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a being Element of F st - a = 0. F holds
a = 0. F
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of F st - a = 0. F holds
a = 0. F
let a be Element of F; ::_thesis: ( - a = 0. F implies a = 0. F )
 - (- a) = a by RLVECT_1:17;
hence  ( - a = 0. F implies a = 0. F ) by RLVECT_1:12; ::_thesis: verum
end;

theorem :: VECTSP_1:29
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F st a - b = 0. F holds
b - a = 0. F
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b being Element of F st a - b = 0. F holds
b - a = 0. F
let a, b be Element of F; ::_thesis: ( a - b = 0. F implies b - a = 0. F )
 a - b = - (b - a) by RLVECT_1:33;
hence  ( a - b = 0. F implies b - a = 0. F ) by Th28; ::_thesis: verum
end;

theorem :: VECTSP_1:30
for F being Field
for a, b, c being Element of F holds
( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )
proof
let F be Field; ::_thesis: for a, b, c being Element of F holds
( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )
let a, b, c be Element of F; ::_thesis: ( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )
thus A1: ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) ::_thesis: ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") )
proof
assume  a <> 0. F ; ::_thesis: ( not (a * c) - b = 0. F or c = b * (a ") )
then A2: (a ") * a = 1. F by Def10;
assume  (a * c) - b = 0. F ; ::_thesis: c = b * (a ")
then  (a ") * (a * c) = b * (a ") by RLVECT_1:21;
then  ((a ") * a) * c = b * (a ") by GROUP_1:def_3;
hence  c = b * (a ") by A2, Def6; ::_thesis: verum
end;
assume A3: a <> 0. F ; ::_thesis: ( not b - (c * a) = 0. F or c = b * (a ") )
assume  b - (c * a) = 0. F ; ::_thesis: c = b * (a ")
then  - (b - (c * a)) = 0. F by RLVECT_1:12;
hence  c = b * (a ") by A1, A3, RLVECT_1:33; ::_thesis: verum
end;

theorem :: VECTSP_1:31
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F holds a + b = - ((- b) + (- a))
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b being Element of F holds a + b = - ((- b) + (- a))
let a, b be Element of F; ::_thesis: a + b = - ((- b) + (- a))
thus a + b = - (- (a + b)) by RLVECT_1:17
.= - ((- b) + (- a)) by RLVECT_1:31 ; ::_thesis: verum
end;

theorem :: VECTSP_1:32
for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b, c being Element of F holds (b + a) - (c + a) = b - c
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b, c being Element of F holds (b + a) - (c + a) = b - c
let a, b, c be Element of F; ::_thesis: (b + a) - (c + a) = b - c
thus (b + a) - (c + a) = (b + a) + ((- a) + (- c)) by RLVECT_1:31
.= ((b + a) + (- a)) + (- c) by RLVECT_1:def_3
.= (b + (a + (- a))) + (- c) by RLVECT_1:def_3
.= (b + (0. F)) + (- c) by RLVECT_1:5
.= b - c by RLVECT_1:4 ; ::_thesis: verum
end;

theorem :: VECTSP_1:33
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of G holds - ((- v) + w) = (- w) + v
proof
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, w being Element of G holds - ((- v) + w) = (- w) + v
let v, w be Element of G; ::_thesis: - ((- v) + w) = (- w) + v
thus  - ((- v) + w) = (- w) + (- (- v)) by RLVECT_1:31
.= (- w) + v by RLVECT_1:17 ; ::_thesis: verum
end;

theorem :: VECTSP_1:34
for G being non empty Abelian add-associative addLoopStr
for u, v, w being Element of G holds (u - v) - w = (u - w) - v
proof
let G be non empty Abelian add-associative addLoopStr ; ::_thesis: for u, v, w being Element of G holds (u - v) - w = (u - w) - v
let u, v, w be Element of G; ::_thesis: (u - v) - w = (u - w) - v
thus (u - v) - w = (u + (- v)) + (- w)
.= (u + (- w)) + (- v) by RLVECT_1:def_3
.= (u - w) - v ; ::_thesis: verum
end;

theorem :: VECTSP_1:35
for B being AbGroup holds multMagma(# the carrier of B, the addF of B #) is commutative Group
proof
let B be AbGroup; ::_thesis: multMagma(# the carrier of B, the addF of B #) is commutative Group
set G = multMagma(# the carrier of B, the addF of B #);
A1: for a, b being Element of multMagma(# the carrier of B, the addF of B #)
for x, y being Element of B st a = x & b = y holds
a * b = x + y ;
A2: ( multMagma(# the carrier of B, the addF of B #) is associative & multMagma(# the carrier of B, the addF of B #) is Group-like )
proof
reconsider e = 0. B as Element of multMagma(# the carrier of B, the addF of B #) ;
thus  for a, b, c being Element of multMagma(# the carrier of B, the addF of B #) holds (a * b) * c = a * (b * c) :: according to GROUP_1:def_3 ::_thesis: multMagma(# the carrier of B, the addF of B #) is Group-like
proof
let a, b, c be Element of multMagma(# the carrier of B, the addF of B #); ::_thesis: (a * b) * c = a * (b * c)
reconsider x = a, y = b, z = c as Element of B ;
thus (a * b) * c = (x + y) + z
.= x + (y + z) by RLVECT_1:def_3
.= a * (b * c) ; ::_thesis: verum
end;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( b1 * b2 = e & b2 * b1 = e ) )
let a be Element of multMagma(# the carrier of B, the addF of B #); ::_thesis: ( a * e = a & e * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( a * b1 = e & b1 * a = e ) )
reconsider x = a as Element of B ;
thus a * e = x + (0. B)
.= a by RLVECT_1:4 ; ::_thesis: ( e * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( a * b1 = e & b1 * a = e ) )
reconsider b = - x as Element of multMagma(# the carrier of B, the addF of B #) ;
thus e * a = x + (0. B) by A1
.= a by RLVECT_1:4 ; ::_thesis: ex b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( a * b1 = e & b1 * a = e )
take  b ; ::_thesis: ( a * b = e & b * a = e )
thus a * b = x + (- x)
.= e by RLVECT_1:5 ; ::_thesis: b * a = e
thus b * a = x + (- x) by A1
.= e by RLVECT_1:5 ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_Element_of_multMagma(#_the_carrier_of_B,_the_addF_of_B_#)_holds_a_*_b_=_b_*_a
let a, b be Element of multMagma(# the carrier of B, the addF of B #); ::_thesis: a * b = b * a
reconsider x = a, y = b as Element of B ;
thus a * b = y + x by A1
.= b * a ; ::_thesis: verum
end;
hence  multMagma(# the carrier of B, the addF of B #) is commutative Group by A2, GROUP_1:def_12; ::_thesis: verum
end;

begin

theorem :: VECTSP_1:36
for L being non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr
for n being Element of NAT st n > 0 holds
(power L) . ((0. L),n) = 0. L
proof
let L be non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr ; ::_thesis: for n being Element of NAT st n > 0 holds
(power L) . ((0. L),n) = 0. L
let n be Element of NAT ; ::_thesis: ( n > 0 implies (power L) . ((0. L),n) = 0. L )
assume  n > 0 ; ::_thesis: (power L) . ((0. L),n) = 0. L
then  n >= 0 + 1 by NAT_1:13;
then A1: n - 1 >= 0 by XREAL_1:19;
n = (n - 1) + 1
.= (n -' 1) + 1 by A1, XREAL_0:def_2 ;
hence (power L) . ((0. L),n) = ((power L) . ((0. L),(n -' 1))) * (0. L) by GROUP_1:def_7
.= 0. L by Th6 ;
::_thesis: verum
end;

registration
cluster non empty well-unital for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st b1 is well-unital
proof
take  F_Real ; ::_thesis: F_Real is well-unital
thus  F_Real is well-unital ; ::_thesis: verum
end;
end;

registration
let S be non empty well-unital multLoopStr ;
identify 1_ S with  1. S;
compatibility
 1_ S = 1. S by Lm2;
end;

theorem :: VECTSP_1:37
for L being non empty multLoopStr st L is well-unital holds
1. L = 1_ L by Lm2;

definition
let G, H be non empty addMagma ;
let f be Function of G,H;
attrf is additive  means :: VECTSP_1:def 20
 for x, y being Element of G holds f . (x + y) = (f . x) + (f . y);
end;

:: deftheorem  defines additive VECTSP_1:def_20_:_
 for G, H being non empty addMagma
for f being Function of G,H holds
( f is additive iff for x, y being Element of G holds f . (x + y) = (f . x) + (f . y) );