:: ALGSTR_2 semantic presentation

Lemma1: for b1, b2 being Element of F_Real
for b3, b4 being Real holds
( b1 = b3 & b2 = b4 implies b1 * b2 = b3 * b4 )
proof
let c1, c2 be Element of F_Real ;
let c3, c4 be Real;
assume ( c1 = c3 & c2 = c4 ) ;
hence c1 * c2 = multreal . c3,c4 by GROUP_1:def 1, VECTSP_1:def 15
.= c3 * c4 by BINOP_2:def 11 ;

end;

Lemma2: 0 = 0. F_Real
by RLVECT_1:def 2, VECTSP_1:def 15;

Lemma3: for b1, b2 being Element of F_Real holds
not ( b1 <> 0. F_Real & ( for b3 being Element of F_Real holds
not b1 * b3 = b2 ) )
proof
let c1, c2 be Element of F_Real ;
assume E4: c1 <> 0. F_Real ;
reconsider c3 = c1, c4 = c2 as Real by VECTSP_1:def 15;
consider c5 being Real such that
E5: c3 * c5 = c4 by E4, Lemma2, ALGSTR_1:32;
reconsider c6 = c5 as Element of F_Real by VECTSP_1:def 15;
c1 * c6 = c2 by E5, Lemma1;
hence ex b1 being Element of F_Real st c1 * b1 = c2 ;
end;

Lemma4: for b1, b2 being Element of F_Real holds
not ( b1 <> 0. F_Real & ( for b3 being Element of F_Real holds
not b3 * b1 = b2 ) )
proof
let c1, c2 be Element of F_Real ;
assume c1 <> 0. F_Real ;
then consider c3 being Element of F_Real such that
E5: c1 * c3 = c2 by Lemma3;
thus ex b1 being Element of F_Real st b1 * c1 = c2 by E5;
end;

Lemma5: for b1, b2, b3 being Element of F_Real holds
( b1 <> 0. F_Real & b1 * b2 = b1 * b3 implies b2 = b3 )
by VECTSP_1:33;

Lemma6: for b1, b2, b3 being Element of F_Real holds
( b1 <> 0. F_Real & b2 * b1 = b3 * b1 implies b2 = b3 )
by VECTSP_1:33;

Lemma7: for b1 being Element of F_Real holds b1 * (0. F_Real ) = 0. F_Real
by VECTSP_1:44;

Lemma8: for b1 being Element of F_Real holds (0. F_Real ) * b1 = 0. F_Real
by VECTSP_1:44;

registration
cluster F_Real -> multLoop_0-like ;
coherence
F_Real is multLoop_0-like by Lemma3, Lemma4, Lemma5, Lemma6, Lemma7, Lemma8, ALGSTR_1:34;
end;

definition
let c1 be non empty add-left-cancelable add-right-invertible LoopStr ;
let c2 be Element of c1;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func - c2 -> Element of a1 means :Def7: :: ALGSTR_2:def 7
a2 + a3 = 0. a1;
existence
ex b1 being Element of c1 st c2 + b1 = 0. c1 by ALGSTR_1:def 9;
uniqueness
for b1, b2 being Element of c1 holds
( c2 + b1 = 0. c1 & c2 + b2 = 0. c1 implies b1 = b2 ) by ALGSTR_1:def 6;
end;

:: deftheorem Def1 ALGSTR_2:def 1 :
canceled;

:: deftheorem Def2 ALGSTR_2:def 2 :
canceled;

:: deftheorem Def3 ALGSTR_2:def 3 :
canceled;

:: deftheorem Def4 ALGSTR_2:def 4 :
canceled;

:: deftheorem Def5 ALGSTR_2:def 5 :
canceled;

:: deftheorem Def6 ALGSTR_2:def 6 :
canceled;

:: deftheorem Def7 defines - ALGSTR_2:def 7 :
for b1 being non empty add-left-cancelable add-right-invertible LoopStr
for b2, b3 being Element of b1 holds
( b3 = - b2 iff b2 + b3 = 0. b1 );

definition
let c1 be non empty add-left-cancelable add-right-invertible LoopStr ;
let c2, c3 be Element of c1;
func c2 - c3 -> Element of a1 equals :: ALGSTR_2:def 8
a2 + (- a3);
correctness
coherence
c2 + (- c3) is Element of c1;
;
end;

:: deftheorem Def8 defines - ALGSTR_2:def 8 :
for b1 being non empty add-left-cancelable add-right-invertible LoopStr
for b2, b3 being Element of b1 holds b2 - b3 = b2 + (- b3);

registration
cluster non empty Abelian add-associative right_zeroed unital associative commutative strict distributive non degenerated left_zeroed Loop-like multLoop_0-like doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is commutative & b1 is associative & b1 is distributive & not b1 is degenerated & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like & b1 is unital & b1 is multLoop_0-like )
proof
take F_Real ;
thus ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is commutative & F_Real is associative & F_Real is distributive & not F_Real is degenerated & F_Real is left_zeroed & F_Real is right_zeroed & F_Real is Loop-like & F_Real is unital & F_Real is multLoop_0-like ) ;
end;
end;

definition
mode doubleLoop is non empty right_zeroed unital left_zeroed Loop-like multLoop_0-like doubleLoopStr ;
end;

definition
mode leftQuasi-Field is Abelian add-associative right-distributive non degenerated doubleLoop;
end;

theorem Th1: :: ALGSTR_2:1
canceled;

theorem Th2: :: ALGSTR_2:2
canceled;

theorem Th3: :: ALGSTR_2:3
canceled;

theorem Th4: :: ALGSTR_2:4
canceled;

theorem Th5: :: ALGSTR_2:5
canceled;

theorem Th6: :: ALGSTR_2:6
canceled;

theorem Th7: :: ALGSTR_2:7
canceled;

theorem Th8: :: ALGSTR_2:8
canceled;

theorem Th9: :: ALGSTR_2:9
canceled;

theorem Th10: :: ALGSTR_2:10
canceled;

theorem Th11: :: ALGSTR_2:11
canceled;

theorem Th12: :: ALGSTR_2:12
for b1 being non empty doubleLoopStr holds
( b1 is leftQuasi-Field iff ( ( for b2 being Element of b1 holds b2 + (0. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 + b3 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) ) & ( for b2, b3 being Element of b1 holds b2 + b3 = b3 + b2 ) & 0. b1 <> 1. b1 & ( for b2 being Element of b1 holds b2 * (1. b1) = b2 ) & ( for b2 being Element of b1 holds (1. b1) * b2 = b2 ) & ( for b2, b3 being Element of b1 holds
not ( b2 <> 0. b1 & ( for b4 being Element of b1 holds
not b2 * b4 = b3 ) ) ) & ( for b2, b3 being Element of b1 holds
not ( b2 <> 0. b1 & ( for b4 being Element of b1 holds
not b4 * b2 = b3 ) ) ) & ( for b2, b3, b4 being Element of b1 holds
( b2 <> 0. b1 & b2 * b3 = b2 * b4 implies b3 = b4 ) ) & ( for b2, b3, b4 being Element of b1 holds
( b2 <> 0. b1 & b3 * b2 = b4 * b2 implies b3 = b4 ) ) & ( for b2 being Element of b1 holds b2 * (0. b1) = 0. b1 ) & ( for b2 being Element of b1 holds (0. b1) * b2 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) ) ) )
proof
let c1 be non empty doubleLoopStr ;
thus ( c1 is leftQuasi-Field implies ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) & ( for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 ) & 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds (1. c1) * b1 = b1 ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b1 * b3 = b2 ) ) ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b3 * b1 = b2 ) ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b2 * b1 = b3 * b1 implies b2 = b3 ) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) ) ) ) by ALGSTR_1:7, ALGSTR_1:34, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 11, VECTSP_1:def 21, VECTSP_1:def 13, VECTSP_1:def 19;
assume E10: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) & ( for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 ) & 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds (1. c1) * b1 = b1 ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b1 * b3 = b2 ) ) ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b3 * b1 = b2 ) ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b2 * b1 = b3 * b1 implies b2 = b3 ) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) ) ) ;
now
thus E11: for b1 being Element of c1 holds (0. c1) + b1 = b1
proof
let c2 be Element of c1;
thus (0. c1) + c2 = c2 + (0. c1) by E10
.= c2 by E10 ;
end;
thus E12: for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E13: c2 + c4 = 0. c1 by E10;
take c5 = c4 + c3;
thus c2 + c5 = (0. c1) + c3 by E10, E13
.= c3 by E11 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E13: c2 + c4 = c3 by E12;
take c4 ;
thus c4 + c2 = c3 by E10, E13;
end;
thus E13: for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E14: c5 + c2 = 0. c1 by E10, ALGSTR_1:3;
assume c2 + c3 = c2 + c4 ;
then (c5 + c2) + c3 = c5 + (c2 + c4) by E10
.= (c5 + c2) + c4 by E10 ;
hence c3 = (0. c1) + c4 by E11, E14
.= c4 by E11 ;

end;
thus for b1, b2, b3 being Element of c1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
assume c3 + c2 = c4 + c2 ;
then c2 + c3 = c4 + c2 by E10
.= c2 + c4 by E10 ;
hence c3 = c4 by E13;
end;
end;
hence c1 is leftQuasi-Field by E10, ALGSTR_1:7, ALGSTR_1:34, ALGSTR_1:def 5, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 11, VECTSP_1:def 21, GROUP_1:def 2;
end;

theorem Th13: :: ALGSTR_2:13
canceled;

theorem Th14: :: ALGSTR_2:14
for b1 being Abelian right-distributive doubleLoop
for b2, b3 being Element of b1 holds b2 * (- b3) = - (b2 * b3)
proof
let c1 be Abelian right-distributive doubleLoop;
let c2, c3 be Element of c1;
(c2 * c3) + (c2 * (- c3)) = c2 * (c3 + (- c3)) by VECTSP_1:def 11
.= c2 * (0. c1) by Def7
.= 0. c1 by ALGSTR_1:34 ;
hence c2 * (- c3) = - (c2 * c3) by Def7;
end;

theorem Th15: :: ALGSTR_2:15
for b1 being non empty Abelian add-left-cancelable add-right-invertible LoopStr
for b2 being Element of b1 holds - (- b2) = b2
proof
let c1 be non empty Abelian add-left-cancelable add-right-invertible LoopStr ;
let c2 be Element of c1;
(- c2) + c2 = 0. c1 by Def7;
hence - (- c2) = c2 by Def7;
end;

theorem Th16: :: ALGSTR_2:16
for b1 being Abelian right-distributive doubleLoop holds (- (1. b1)) * (- (1. b1)) = 1. b1
proof
let c1 be Abelian right-distributive doubleLoop;
thus (- (1. c1)) * (- (1. c1)) = - ((- (1. c1)) * (1. c1)) by Th14
.= - (- (1. c1)) by VECTSP_1:def 13
.= 1. c1 by Th15 ;
end;

theorem Th17: :: ALGSTR_2:17
for b1 being Abelian right-distributive doubleLoop
for b2, b3, b4 being Element of b1 holds b2 * (b3 - b4) = (b2 * b3) - (b2 * b4)
proof
let c1 be Abelian right-distributive doubleLoop;
let c2, c3, c4 be Element of c1;
thus c2 * (c3 - c4) = c2 * (c3 + (- c4))
.= (c2 * c3) + (c2 * (- c4)) by VECTSP_1:def 11
.= (c2 * c3) + (- (c2 * c4)) by Th14
.= (c2 * c3) - (c2 * c4) ;
end;

definition
mode rightQuasi-Field is Abelian add-associative left-distributive non degenerated doubleLoop;
end;

theorem Th18: :: ALGSTR_2:18
canceled;

theorem Th19: :: ALGSTR_2:19
for b1 being non empty doubleLoopStr holds
( b1 is rightQuasi-Field iff ( ( for b2 being Element of b1 holds b2 + (0. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 + b3 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) ) & ( for b2, b3 being Element of b1 holds b2 + b3 = b3 + b2 ) & 0. b1 <> 1. b1 & ( for b2 being Element of b1 holds b2 * (1. b1) = b2 ) & ( for b2 being Element of b1 holds (1. b1) * b2 = b2 ) & ( for b2, b3 being Element of b1 holds
not ( b2 <> 0. b1 & ( for b4 being Element of b1 holds
not b2 * b4 = b3 ) ) ) & ( for b2, b3 being Element of b1 holds
not ( b2 <> 0. b1 & ( for b4 being Element of b1 holds
not b4 * b2 = b3 ) ) ) & ( for b2, b3, b4 being Element of b1 holds
( b2 <> 0. b1 & b2 * b3 = b2 * b4 implies b3 = b4 ) ) & ( for b2, b3, b4 being Element of b1 holds
( b2 <> 0. b1 & b3 * b2 = b4 * b2 implies b3 = b4 ) ) & ( for b2 being Element of b1 holds b2 * (0. b1) = 0. b1 ) & ( for b2 being Element of b1 holds (0. b1) * b2 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b3 + b4) * b2 = (b3 * b2) + (b4 * b2) ) ) )
proof
let c1 be non empty doubleLoopStr ;
thus ( c1 is rightQuasi-Field implies ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) & ( for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 ) & 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds (1. c1) * b1 = b1 ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b1 * b3 = b2 ) ) ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b3 * b1 = b2 ) ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b2 * b1 = b3 * b1 implies b2 = b3 ) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) ) ) ) by ALGSTR_1:7, ALGSTR_1:34, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 12, VECTSP_1:def 21, VECTSP_1:def 13, VECTSP_1:def 19;
assume E12: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) & ( for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 ) & 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds (1. c1) * b1 = b1 ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b1 * b3 = b2 ) ) ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b3 * b1 = b2 ) ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b2 * b1 = b3 * b1 implies b2 = b3 ) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) ) ) ;
now
thus E13: for b1 being Element of c1 holds (0. c1) + b1 = b1
proof
let c2 be Element of c1;
thus (0. c1) + c2 = c2 + (0. c1) by E12
.= c2 by E12 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E14: c2 + c4 = 0. c1 by E12;
take c5 = c4 + c3;
thus c2 + c5 = (0. c1) + c3 by E12, E14
.= c3 by E13 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E14: c4 + c2 = 0. c1 by E12, ALGSTR_1:3;
take c5 = c3 + c4;
thus c5 + c2 = c3 + (0. c1) by E12, E14
.= c3 by E12 ;
end;
thus for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E14: c5 + c2 = 0. c1 by E12, ALGSTR_1:3;
assume c2 + c3 = c2 + c4 ;
then (c5 + c2) + c3 = c5 + (c2 + c4) by E12
.= (c5 + c2) + c4 by E12 ;
hence c3 = (0. c1) + c4 by E13, E14
.= c4 by E13 ;

end;
thus for b1, b2, b3 being Element of c1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E14: c2 + c5 = 0. c1 by E12;
assume c3 + c2 = c4 + c2 ;
then c3 + (c2 + c5) = (c4 + c2) + c5 by E12
.= c4 + (c2 + c5) by E12 ;
hence c3 = c4 + (0. c1) by E12, E14
.= c4 by E12 ;

end;
end;
hence c1 is rightQuasi-Field by E12, ALGSTR_1:7, ALGSTR_1:34, ALGSTR_1:def 5, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 12, VECTSP_1:def 21, GROUP_1:def 2;
end;

theorem Th20: :: ALGSTR_2:20
canceled;

theorem Th21: :: ALGSTR_2:21
for b1 being left-distributive doubleLoop
for b2, b3 being Element of b1 holds (- b2) * b3 = - (b2 * b3)
proof
let c1 be left-distributive doubleLoop;
let c2, c3 be Element of c1;
(c2 * c3) + ((- c2) * c3) = (c2 + (- c2)) * c3 by VECTSP_1:def 12
.= (0. c1) * c3 by Def7
.= 0. c1 by ALGSTR_1:34 ;
hence (- c2) * c3 = - (c2 * c3) by Def7;
end;

theorem Th22: :: ALGSTR_2:22
canceled;

theorem Th23: :: ALGSTR_2:23
for b1 being Abelian left-distributive doubleLoop holds (- (1. b1)) * (- (1. b1)) = 1. b1
proof
let c1 be Abelian left-distributive doubleLoop;
thus (- (1. c1)) * (- (1. c1)) = - ((1. c1) * (- (1. c1))) by Th21
.= - (- (1. c1)) by VECTSP_1:def 19
.= 1. c1 by Th15 ;
end;

theorem Th24: :: ALGSTR_2:24
for b1 being left-distributive doubleLoop
for b2, b3, b4 being Element of b1 holds (b2 - b3) * b4 = (b2 * b4) - (b3 * b4)
proof
let c1 be left-distributive doubleLoop;
let c2, c3, c4 be Element of c1;
thus (c2 - c3) * c4 = (c2 + (- c3)) * c4
.= (c2 * c4) + ((- c3) * c4) by VECTSP_1:def 12
.= (c2 * c4) + (- (c3 * c4)) by Th21
.= (c2 * c4) - (c3 * c4) ;
end;

definition
mode doublesidedQuasi-Field is Abelian add-associative distributive non degenerated doubleLoop;
end;

theorem Th25: :: ALGSTR_2:25
canceled;

theorem Th26: :: ALGSTR_2:26
for b1 being non empty doubleLoopStr holds
( b1 is doublesidedQuasi-Field iff ( ( for b2 being Element of b1 holds b2 + (0. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 + b3 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) ) & ( for b2, b3 being Element of b1 holds b2 + b3 = b3 + b2 ) & 0. b1 <> 1. b1 & ( for b2 being Element of b1 holds b2 * (1. b1) = b2 ) & ( for b2 being Element of b1 holds (1. b1) * b2 = b2 ) & ( for b2, b3 being Element of b1 holds
not ( b2 <> 0. b1 & ( for b4 being Element of b1 holds
not b2 * b4 = b3 ) ) ) & ( for b2, b3 being Element of b1 holds
not ( b2 <> 0. b1 & ( for b4 being Element of b1 holds
not b4 * b2 = b3 ) ) ) & ( for b2, b3, b4 being Element of b1 holds
( b2 <> 0. b1 & b2 * b3 = b2 * b4 implies b3 = b4 ) ) & ( for b2, b3, b4 being Element of b1 holds
( b2 <> 0. b1 & b3 * b2 = b4 * b2 implies b3 = b4 ) ) & ( for b2 being Element of b1 holds b2 * (0. b1) = 0. b1 ) & ( for b2 being Element of b1 holds (0. b1) * b2 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds b2 * (b3 + b4) = (b2 * b3) + (b2 * b4) ) & ( for b2, b3, b4 being Element of b1 holds (b3 + b4) * b2 = (b3 * b2) + (b4 * b2) ) ) )
proof
let c1 be non empty doubleLoopStr ;
thus ( c1 is doublesidedQuasi-Field implies ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) & ( for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 ) & 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds (1. c1) * b1 = b1 ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b1 * b3 = b2 ) ) ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b3 * b1 = b2 ) ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b2 * b1 = b3 * b1 implies b2 = b3 ) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) ) & ( for b1, b2, b3 being Element of c1 holds (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) ) ) ) by ALGSTR_1:7, ALGSTR_1:34, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 18, VECTSP_1:def 21, VECTSP_1:def 13, VECTSP_1:def 19;
assume E13: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) & ( for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 ) & 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds (1. c1) * b1 = b1 ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b1 * b3 = b2 ) ) ) & ( for b1, b2 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b3 being Element of c1 holds
not b3 * b1 = b2 ) ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b1 <> 0. c1 & b2 * b1 = b3 * b1 implies b2 = b3 ) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) ) & ( for b1, b2, b3 being Element of c1 holds (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) ) ) ;
now
thus E14: for b1 being Element of c1 holds (0. c1) + b1 = b1
proof
let c2 be Element of c1;
thus (0. c1) + c2 = c2 + (0. c1) by E13
.= c2 by E13 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E15: c2 + c4 = 0. c1 by E13;
take c5 = c4 + c3;
thus c2 + c5 = (0. c1) + c3 by E13, E15
.= c3 by E14 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E15: c4 + c2 = 0. c1 by E13, ALGSTR_1:3;
take c5 = c3 + c4;
thus c5 + c2 = c3 + (0. c1) by E13, E15
.= c3 by E13 ;
end;
thus for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E15: c5 + c2 = 0. c1 by E13, ALGSTR_1:3;
assume c2 + c3 = c2 + c4 ;
then (c5 + c2) + c3 = c5 + (c2 + c4) by E13
.= (c5 + c2) + c4 by E13 ;
hence c3 = (0. c1) + c4 by E14, E15
.= c4 by E14 ;

end;
thus for b1, b2, b3 being Element of c1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E15: c2 + c5 = 0. c1 by E13;
assume c3 + c2 = c4 + c2 ;
then c3 + (c2 + c5) = (c4 + c2) + c5 by E13
.= c4 + (c2 + c5) by E13 ;
hence c3 = c4 + (0. c1) by E13, E15
.= c4 by E13 ;

end;
end;
hence c1 is doublesidedQuasi-Field by E13, ALGSTR_1:7, ALGSTR_1:34, ALGSTR_1:def 5, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 18, VECTSP_1:def 21, GROUP_1:def 2;
end;

definition
mode _Skew-Field is associative doublesidedQuasi-Field;
end;

Lemma13: for b1 being non empty doubleLoopStr
for b2, b3 being Element of b1 holds
( 0. b1 <> 1. b1 & ( for b4 being Element of b1 holds b4 * (1. b1) = b4 ) & ( for b4 being Element of b1 holds
not ( b4 <> 0. b1 & ( for b5 being Element of b1 holds
not b4 * b5 = 1. b1 ) ) ) & ( for b4, b5, b6 being Element of b1 holds (b4 * b5) * b6 = b4 * (b5 * b6) ) & ( for b4 being Element of b1 holds b4 * (0. b1) = 0. b1 ) & ( for b4 being Element of b1 holds (0. b1) * b4 = 0. b1 ) & b2 * b3 = 1. b1 implies b3 * b2 = 1. b1 )
proof
let c1 be non empty doubleLoopStr ;
let c2, c3 be Element of c1;
assume E14: ( 0. c1 <> 1. c1 & ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds
not ( b1 <> 0. c1 & ( for b2 being Element of c1 holds
not b1 * b2 = 1. c1 ) ) ) & ( for b1, b2, b3 being Element of c1 holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of c1 holds b1 * (0. c1) = 0. c1 ) & ( for b1 being Element of c1 holds (0. c1) * b1 = 0. c1 ) ) ;
thus ( c2 * c3 = 1. c1 implies c3 * c2 = 1. c1 )
proof
assume E15: c2 * c3 = 1. c1 ;
then c3 <> 0. c1 by E14;
then consider c4 being Element of c1 such that
E16: c3 * c4 = 1. c1 by E14;
thus c3 * c2 = (c3 * c2) * (c3 * c4) by E14, E16
.= ((c3 * c2) * c3) * c4 by E14
.= (c3 * (1. c1)) * c4 by E14, E15
.= 1. c1 by E14,