:: MIDSP_1 semantic presentation

definition
attr a1 is strict;
struct MidStr -> 1-sorted ;
aggr MidStr(# carrier, MIDPOINT #) -> MidStr ;
sel MIDPOINT c1 -> BinOp of the carrier of a1;
end;

registration
cluster non empty MidStr ;
existence
not for b1 being MidStr holds b1 is empty
proof end;
end;

definition
let c1 be non empty MidStr ;
let c2, c3 be Element of c1;
func c2 @ c3 -> Element of a1 equals :: MIDSP_1:def 1
the MIDPOINT of a1 . a2,a3;
coherence
the MIDPOINT of c1 . c2,c3 is Element of c1 ;
end;

:: deftheorem Def1 defines @ MIDSP_1:def 1 :
for b1 being non empty MidStr
for b2, b3 being Element of b1 holds b2 @ b3 = the MIDPOINT of b1 . b2,b3;

definition
func op2 -> BinOp of {{} } means :: MIDSP_1:def 2
verum;
existence
ex b1 being BinOp of {{} } st verum ;
uniqueness
for b1, b2 being BinOp of {{} } holds b1 = b2 by FUNCT_2:66;
end;

:: deftheorem Def2 defines op2 MIDSP_1:def 2 :
for b1 being BinOp of {{} } holds
( b1 = op2 iff verum );

definition
func Example -> MidStr equals :: MIDSP_1:def 3
 MidStr(# {{} },op2 #);
correctness
coherence
MidStr(# {{} },op2 #) is MidStr ;
;
end;

:: deftheorem Def3 defines Example MIDSP_1:def 3 :
Example = MidStr(# {{} },op2 #);

registration
cluster Example -> non empty strict ;
coherence
( Example is strict & not Example is empty )
proof end;
end;

theorem Th1: :: MIDSP_1:1
canceled;

theorem Th2: :: MIDSP_1:2
canceled;

theorem Th3: :: MIDSP_1:3
canceled;

theorem Th4: :: MIDSP_1:4
canceled;

theorem Th5: :: MIDSP_1:5
the carrier of Example = {{} } ;

theorem Th6: :: MIDSP_1:6
the MIDPOINT of Example = op2 ;

theorem Th7: :: MIDSP_1:7
for b1 being Element of Example holds b1 = {} by TARSKI:def 1;

theorem Th8: :: MIDSP_1:8
for b1, b2 being Element of Example holds b1 @ b2 = op2 . b1,b2 ;

theorem Th9: :: MIDSP_1:9
canceled;

theorem Th10: :: MIDSP_1:10
for b1, b2, b3, b4 being Element of Example holds
( b1 @ b1 = b1 & b1 @ b2 = b2 @ b1 & (b1 @ b2) @ (b3 @ b4) = (b1 @ b3) @ (b2 @ b4) & ex b5 being Element of Example st b5 @ b1 = b2 )
proof end;

definition
let c1 be non empty MidStr ;
attr a1 is MidSp-like means :Def4: :: MIDSP_1:def 4
for b1, b2, b3, b4 being Element of a1 holds
( b1 @ b1 = b1 & b1 @ b2 = b2 @ b1 & (b1 @ b2) @ (b3 @ b4) = (b1 @ b3) @ (b2 @ b4) & ex b5 being Element of a1 st b5 @ b1 = b2 );
end;

:: deftheorem Def4 defines MidSp-like MIDSP_1:def 4 :
for b1 being non empty MidStr holds
( b1 is MidSp-like iff for b2, b3, b4, b5 being Element of b1 holds
( b2 @ b2 = b2 & b2 @ b3 = b3 @ b2 & (b2 @ b3) @ (b4 @ b5) = (b2 @ b4) @ (b3 @ b5) & ex b6 being Element of b1 st b6 @ b2 = b3 ) );

registration
cluster non empty strict MidSp-like MidStr ;
existence
ex b1 being non empty MidStr st
( b1 is strict & b1 is MidSp-like )
proof end;
end;

definition
mode MidSp is non empty MidSp-like MidStr ;
end;

definition
let c1 be MidSp;
let c2, c3 be Element of c1;
redefine func @ as c2 @ c3 -> Element of a1;
commutativity
for b1, b2 being Element of c1 holds b1 @ b2 = b2 @ b1 by Def4;
end;

theorem Th11: :: MIDSP_1:11
canceled;

theorem Th12: :: MIDSP_1:12
canceled;

theorem Th13: :: MIDSP_1:13
canceled;

theorem Th14: :: MIDSP_1:14
canceled;

theorem Th15: :: MIDSP_1:15
for b1 being MidSp
for b2, b3, b4 being Element of b1 holds (b2 @ b3) @ b4 = (b2 @ b4) @ (b3 @ b4)
proof end;

theorem Th16: :: MIDSP_1:16
for b1 being MidSp
for b2, b3, b4 being Element of b1 holds b2 @ (b3 @ b4) = (b2 @ b3) @ (b2 @ b4)
proof end;

theorem Th17: :: MIDSP_1:17
for b1 being MidSp
for b2, b3 being Element of b1 st b2 @ b3 = b2 holds
b2 = b3
proof end;

theorem Th18: :: MIDSP_1:18
for b1 being MidSp
for b2, b3, b4 being Element of b1 st b2 @ b3 = b4 @ b3 holds
b2 = b4
proof end;

theorem Th19: :: MIDSP_1:19
for b1 being MidSp
for b2, b3, b4 being Element of b1 st b2 @ b3 = b2 @ b4 holds
b3 = b4 by Th18;

definition
let c1 be MidSp;
let c2, c3, c4, c5 be Element of c1;
pred c2,c3 @@ c4,c5 means :Def5: :: MIDSP_1:def 5
a2 @ a5 = a3 @ a4;
end;

:: deftheorem Def5 defines @@ MIDSP_1:def 5 :
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 @@ b4,b5 iff b2 @ b5 = b3 @ b4 );

theorem Th20: :: MIDSP_1:20
canceled;

theorem Th21: :: MIDSP_1:21
for b1 being MidSp
for b2, b3 being Element of b1 holds b2,b2 @@ b3,b3
proof end;

theorem Th22: :: MIDSP_1:22
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 @@ b4,b5 holds
b4,b5 @@ b2,b3
proof end;

theorem Th23: :: MIDSP_1:23
for b1 being MidSp
for b2, b3, b4 being Element of b1 st b2,b2 @@ b3,b4 holds
b3 = b4
proof end;

theorem Th24: :: MIDSP_1:24
for b1 being MidSp
for b2, b3, b4 being Element of b1 st b2,b3 @@ b4,b4 holds
b2 = b3
proof end;

theorem Th25: :: MIDSP_1:25
for b1 being MidSp
for b2, b3 being Element of b1 holds b2,b3 @@ b2,b3
proof end;

theorem Th26: :: MIDSP_1:26
for b1 being MidSp
for b2, b3, b4 being Element of b1 ex b5 being Element of b1 st b2,b3 @@ b4,b5
proof end;

theorem Th27: :: MIDSP_1:27
for b1 being MidSp
for b2, b3, b4, b5, b6 being Element of b1 st b2,b3 @@ b4,b5 & b2,b3 @@ b4,b6 holds
b5 = b6
proof end;

theorem Th28: :: MIDSP_1:28
for b1 being MidSp
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 @@ b4,b5 & b2,b3 @@ b6,b7 holds
b4,b5 @@ b6,b7
proof end;

theorem Th29: :: MIDSP_1:29
for b1 being MidSp
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 @@ b4,b5 & b3,b6 @@ b5,b7 holds
b2,b6 @@ b4,b7
proof end;

definition
let c1 be MidSp;
let c2 be Element of [:the carrier of c1,the carrier of c1:];
redefine func `1 as c2 `1 -> Element of a1;
coherence
c2 `1 is Element of c1 by MCART_1:10;
end;

definition
let c1 be MidSp;
let c2 be Element of [:the carrier of c1,the carrier of c1:];
redefine func `2 as c2 `2 -> Element of a1;
coherence
c2 `2 is Element of c1 by MCART_1:10;
end;

definition
let c1 be MidSp;
let c2, c3 be Element of [:the carrier of c1,the carrier of c1:];
pred c2 ## c3 means :Def6: :: MIDSP_1:def 6
a2 `1 ,a2 `2 @@ a3 `1 ,a3 `2 ;
reflexivity
for b1 being Element of [:the carrier of c1,the carrier of c1:] holds b1 `1 ,b1 `2 @@ b1 `1 ,b1 `2 by Th25;
symmetry
for b1, b2 being Element of [:the carrier of c1,the carrier of c1:] st b1 `1 ,b1 `2 @@ b2 `1 ,b2 `2 holds
b2 `1 ,b2 `2 @@ b1 `1 ,b1 `2 by Th22;
end;

:: deftheorem Def6 defines ## MIDSP_1:def 6 :
for b1 being MidSp
for b2, b3 being Element of [:the carrier of b1,the carrier of b1:] holds
( b2 ## b3 iff b2 `1 ,b2 `2 @@ b3 `1 ,b3 `2 );

definition
let c1 be MidSp;
let c2, c3 be Element of c1;
redefine func [ as [c2,c3] -> Element of [:the carrier of a1,the carrier of a1:];
coherence
[c2,c3] is Element of [:the carrier of c1,the carrier of c1:] by ZFMISC_1:def 2;
end;

theorem Th30: :: MIDSP_1:30
canceled;

theorem Th31: :: MIDSP_1:31
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 @@ b4,b5 holds
[b2,b3] ## [b4,b5]
proof end;

theorem Th32: :: MIDSP_1:32
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 st [b2,b3] ## [b4,b5] holds
b2,b3 @@ b4,b5
proof end;

theorem Th33: :: MIDSP_1:33
canceled;

theorem Th34: :: MIDSP_1:34
canceled;

theorem Th35: :: MIDSP_1:35
for b1 being MidSp
for b2, b3, b4 being Element of [:the carrier of b1,the carrier of b1:] st b2 ## b3 & b2 ## b4 holds
b3 ## b4
proof end;

theorem Th36: :: MIDSP_1:36
for b1 being MidSp
for b2, b3, b4 being Element of [:the carrier of b1,the carrier of b1:] st b2 ## b3 & b4 ## b3 holds
b2 ## b4 by Th35;

theorem Th37: :: MIDSP_1:37
for b1 being MidSp
for b2, b3, b4 being Element of [:the carrier of b1,the carrier of b1:] st b2 ## b3 & b3 ## b4 holds
b2 ## b4 by Th35;

theorem Th38: :: MIDSP_1:38
for b1 being MidSp
for b2, b3, b4 being Element of [:the carrier of b1,the carrier of b1:] st b2 ## b3 holds
( b4 ## b2 iff b4 ## b3 ) by Th35;

theorem Th39: :: MIDSP_1:39
for b1 being MidSp
for b2 being Element of [:the carrier of b1,the carrier of b1:] holds { b3 where B is Element of [:the carrier of b1,the carrier of b1:] : b3 ## b2 } is non empty Subset of [:the carrier of b1,the carrier of b1:]
proof end;

definition
let c1 be MidSp;
let c2 be Element of [:the carrier of c1,the carrier of c1:];
func c2 ~ -> Subset of [:the carrier of a1,the carrier of a1:] equals :: MIDSP_1:def 7
{ b1 where B is Element of [:the carrier of a1,the carrier of a1:] : b1 ## a2 } ;
coherence
{ b1 where B is Element of [:the carrier of c1,the carrier of c1:] : b1 ## c2 } is Subset of [:the carrier of c1,the carrier of c1:] by Th39;
end;

:: deftheorem Def7 defines ~ MIDSP_1:def 7 :
for b1 being MidSp
for b2 being Element of [:the carrier of b1,the carrier of b1:] holds b2 ~ = { b3 where B is Element of [:the carrier of b1,the carrier of b1:] : b3 ## b2 } ;

registration
let c1 be MidSp;
let c2 be Element of [:the carrier of c1,the carrier of c1:];
cluster a2 ~ -> non empty ;
coherence
not c2 ~ is empty by Th39;
end;

theorem Th40: :: MIDSP_1:40
canceled;

theorem Th41: :: MIDSP_1:41
for b1 being MidSp
for b2, b3 being Element of [:the carrier of b1,the carrier of b1:] holds
( b2 in b3 ~ iff b2 ## b3 )
proof end;

theorem Th42: :: MIDSP_1:42
for b1 being MidSp
for b2, b3 being Element of [:the carrier of b1,the carrier of b1:] st b2 ## b3 holds
b2 ~ = b3 ~
proof end;

theorem Th43: :: MIDSP_1:43
for b1 being MidSp
for b2, b3 being Element of [:the carrier of b1,the carrier of b1:] st b2 ~ = b3 ~ holds
b2 ## b3
proof end;

theorem Th44: :: MIDSP_1:44
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 st [b2,b3] ~ = [b4,b5] ~ holds
b2 @ b5 = b3 @ b4
proof end;

theorem Th45: :: MIDSP_1:45
for b1 being MidSp
for b2 being Element of [:the carrier of b1,the carrier of b1:] holds b2 in b2 ~ ;

definition
let c1 be MidSp;
mode Vector of c1 -> non empty Subset of [:the carrier of a1,the carrier of a1:] means :Def8: :: MIDSP_1:def 8
ex b1 being Element of [:the carrier of a1,the carrier of a1:] st a2 = b1 ~ ;
existence
ex b1 being non empty Subset of [:the carrier of c1,the carrier of c1:]ex b2 being Element of [:the carrier of c1,the carrier of c1:] st b1 = b2 ~
proof end;
end;

:: deftheorem Def8 defines Vector MIDSP_1:def 8 :
for b1 being MidSp
for b2 being non empty Subset of [:the carrier of b1,the carrier of b1:] holds
( b2 is Vector of b1 iff ex b3 being Element of [:the carrier of b1,the carrier of b1:] st b2 = b3 ~ );

definition
let c1 be MidSp;
let c2 be Element of [:the carrier of c1,the carrier of c1:];
redefine func ~ as c2 ~ -> Vector of a1;
coherence
c2 ~ is Vector of c1 by Def8;
end;

theorem Th46: :: MIDSP_1:46
canceled;

theorem Th47: :: MIDSP_1:47
canceled;

theorem Th48: :: MIDSP_1:48
for b1 being MidSp ex b2 being Vector of b1 st
for b3 being Element of [:the carrier of b1,the carrier of b1:] holds
( b3 in b2 iff b3 `1 = b3 `2 )
proof end;

definition
let c1 be MidSp;
func ID c1 -> Vector of a1 equals :: MIDSP_1:def 9
{ b1 where B is Element of [:the carrier of a1,the carrier of a1:] : b1 `1 = b1 `2 } ;
coherence
{ b1 where B is Element of [:the carrier of c1,the carrier of c1:] : b1 `1 = b1 `2 } is Vector of c1
proof end;
end;

:: deftheorem Def9 defines ID MIDSP_1:def 9 :
for b1 being MidSp holds ID b1 = { b2 where B is Element of [:the carrier of b1,the carrier of b1:] : b2 `1 = b2 `2 } ;

theorem Th49: :: MIDSP_1:49
canceled;

theorem Th50: :: MIDSP_1:50
for b1 being MidSp
for b2 being Element of b1 holds ID b1 = [b2,b2] ~
proof end;

theorem Th51: :: MIDSP_1:51
for b1 being MidSp
for b2, b3 being Vector of b1 ex b4 being Vector of b1ex b5, b6 being Element of [:the carrier of b1,the carrier of b1:] st
( b2 = b5 ~ & b3 = b6 ~ & b5 `2 = b6 `1 & b4 = [(b5 `1 ),(b6 `2 )] ~ )
proof end;

theorem Th52: :: MIDSP_1:52
for b1 being MidSp
for b2, b3, b4, b5 being Vector of b1 st ex b6, b7 being Element of [:the carrier of b1,the carrier of b1:] st
( b2 = b6 ~ & b3 = b7 ~ & b6 `2 = b7 `1 & b4 = [(b6 `1 ),(b7 `2 )] ~ ) & ex b6, b7 being Element of [:the carrier of b1,the carrier of b1:] st
( b2 = b6 ~ & b3 = b7 ~ & b6 `2 = b7 `1 & b5 = [(b6 `1 ),(b7 `2 )] ~ ) holds
b4 = b5
proof end;

definition
let c1 be MidSp;
let c2, c3 be Vector of c1;
func c2 + c3 -> Vector of a1 means :Def10: :: MIDSP_1:def 10
ex b1, b2 being Element of [:the carrier of a1,the carrier of a1:] st
( a2 = b1 ~ & a3 = b2 ~ & b1 `2 = b2 `1 & a4 = [(b1 `1 ),(b2 `2 )] ~ );
existence
ex b1 being Vector of c1ex b2, b3 being Element of [:the carrier of c1,the carrier of c1:] st
( c2 = b2 ~ & c3 = b3 ~ & b2 `2 = b3 `1 & b1 = [(b2 `1 ),(b3 `2 )] ~ ) by Th51;
uniqueness
for b1, b2 being Vector of c1 st ex b3, b4 being Element of [:the carrier of c1,the carrier of c1:] st
( c2 = b3 ~ & c3 = b4 ~ & b3 `2 = b4 `1 & b1 = [(b3 `1 ),(b4 `2 )] ~ ) & ex b3, b4 being Element of [:the carrier of c1,the carrier of c1:] st
( c2 = b3 ~ & c3 = b4 ~ & b3 `2 = b4 `1 & b2 = [(b3 `1 ),(b4 `2 )] ~ ) holds
b1 = b2 by Th52;
end;

:: deftheorem Def10 defines + MIDSP_1:def 10 :
for b1 being MidSp
for b2, b3, b4 being Vector of b1 holds
( b4 = b2 + b3 iff ex b5, b6 being Element of [:the carrier of b1,the carrier of b1:] st
( b2 = b5 ~ & b3 = b6 ~ & b5 `2 = b6 `1 & b4 = [(b5 `1 ),(b6 `2 )] ~ ) );

theorem Th53: :: MIDSP_1:53
for b1 being MidSp
for b2 being Element of b1
for b3 being Vector of b1 ex b4 being Element of b1 st b3 = [b2,b4] ~
proof end;

definition
let c1 be MidSp;
let c2, c3 be Element of c1;
func vect c2,c3 -> Vector of a1 equals :: MIDSP_1:def 11
[a2,a3] ~ ;
coherence
[c2,c3] ~ is Vector of c1 ;
end;

:: deftheorem Def11 defines vect MIDSP_1:def 11 :
for b1 being MidSp
for b2, b3 being Element of b1 holds vect b2,b3 = [b2,b3] ~ ;

theorem Th54: :: MIDSP_1:54
canceled;

theorem Th55: :: MIDSP_1:55
for b1 being MidSp
for b2 being Element of b1
for b3 being Vector of b1 ex b4 being Element of b1 st b3 = vect b2,b4
proof end;

theorem Th56: :: MIDSP_1:56
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 st [b2,b3] ## [b4,b5] holds
vect b2,b3 = vect b4,b5 by Th42;

theorem Th57: :: MIDSP_1:57
for b1 being MidSp
for b2, b3, b4, b5 being Element of b1 st vect b2,b3 = vect b4,b5 holds
b2 @ b5 = b3 @ b4 by Th44;

theorem Th58: :: MIDSP_1:58
for b1 being MidSp
for b2 being Element of b1 holds ID b1 = vect b2,b2 by Th50;

theorem Th59: :: MIDSP_1:59
for b1 being MidSp
for b2, b3, b4 being Element of b1 st vect b2,b3 = vect b2,b4 holds
b3 = b4
proof end;

theorem Th60: :: MIDSP_1:60
for b1 being MidSp
for b2, b3, b4 being Element of b1 holds (vect b2,b3) + (vect b3,b4) = vect b2,b4
proof end;

theorem Th61: :: MIDSP_1:61
for b1 being MidSp
for b2, b3 being Element of b1 holds [b2,(b2 @ b3)] ## [(b2 @ b3),b3]
proof end;

theorem Th62: :: MIDSP_1:62
for b1 being MidSp
for b2, b3 being Element of b1 holds (vect b2,(b2 @ b3)) + (vect b2,(b2 @ b3)) = vect b2,b3
proof end;

theorem Th63: :: MIDSP_1:63
for b1 being MidSp
for b2, b3, b4 being Vector of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4)
proof end;

theorem Th64: :: MIDSP_1:64
for b1 being MidSp
for b2 being Vector of b1 holds b2 + (ID b1) = b2
proof end;

theorem Th65: :: MIDSP_1:65
for b1 being MidSp
for b2 being Vector of b1 ex b3 being Vector of b1 st b2 + b3 = ID b1
proof end;

theorem Th66: :: MIDSP_1:66
for b1 being MidSp
for b2, b3 being Vector of b1 holds b2 + b3 = b3 + b2
proof end;

theorem Th67: :: MIDSP_1:67
for b1 being MidSp
for b2, b3, b4 being Vector of b1 st b2 + b3 = b2 + b4 holds
b3 = b4
proof end;

definition
let c1 be MidSp;
let c2 be Vector of c1;
func - c2 -> Vector of a1 means :: MIDSP_1:def 12
a2 + a3 = ID a1;
existence
ex b1 being Vector of c1 st c2 + b1 = ID c1 by Th65;
uniqueness
for b1, b2 being Vector of c1 st c2 + b1 = ID c1 & c2 + b2 = ID c1 holds
b1 = b2 by Th67;
end;

:: deftheorem Def12 defines - MIDSP_1:def 12 :
for b1 being MidSp
for b2, b3 being Vector of b1 holds
( b3 = - b2 iff b2 + b3 = ID b1 );

definition
let c1 be MidSp;
func setvect c1 -> set equals :: MIDSP_1:def 13
{ b1 where B is Subset of [:the carrier of a1,the carrier of a1:] : b1 is Vector of a1 } ;
coherence
{ b1 where B is Subset of [:the carrier of c1,the carrier of c1:] : b1 is Vector of c1 } is set ;
end;

:: deftheorem Def13 defines setvect MIDSP_1:def 13 :
for b1 being MidSp holds setvect b1 = { b2 where B is Subset of [:the carrier of b1,the carrier of b1:] : b2 is Vector of b1 } ;

theorem Th68: :: MIDSP_1:68
canceled;

theorem Th69: :: MIDSP_1:69
canceled;

theorem Th70: :: MIDSP_1:70
canceled;

theorem Th71: :: MIDSP_1:71
for b1 being MidSp
for b2 being set holds
( b2 is Vector of b1 iff b2 in setvect b1 )
proof end;

registration
let c1 be MidSp;
cluster setvect a1 -> non empty ;
coherence
not setvect c1 is empty
proof end;
end;

definition
let c1 be MidSp;
let c2, c3 be Element of setvect c1;
func c2 + c3 -> Element of setvect a1 means :Def14: :: MIDSP_1:def 14
for b1, b2 being Vector of a1 st a2 = b1 & a3 = b2 holds
a4 = b1 + b2;
existence
ex b1 being Element of setvect c1 st
for b2, b3 being Vector of c1 st c2 = b2 & c3 = b3 holds
b1 = b2 + b3
proof end;
uniqueness
for b1, b2 being Element of setvect c1 st ( for b3, b4 being Vector of c1 st c2 = b3 & c3 = b4 holds
b1 = b3 + b4 ) & ( for b3, b4 being Vector of c1 st c2 = b3 & c3 = b4 holds
b2 = b3 + b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines + MIDSP_1:def 14 :
for b1 being MidSp
for b2, b3, b4 being Element of setvect b1 holds
( b4 = b2 + b3 iff for b5, b6 being Vector of b1 st b2 = b5 & b3 = b6 holds
b4 = b5 + b6 );

theorem Th72: :: MIDSP_1:72
canceled;

theorem Th73: :: MIDSP_1:73
canceled;

theorem Th74: :: MIDSP_1:74
for b1 being MidSp
for b2, b3 being Element of setvect b1 holds b2 + b3 = b3 + b2
proof end;

theorem Th75: :: MIDSP_1:75
for b1 being MidSp
for b2, b3, b4 being Element of setvect b1 holds (b2 + b3) + b4 = b2 + (b3 + b4)
proof end;

definition
let c1 be MidSp;
func addvect c1 -> BinOp of setvect a1 means :Def15: :: MIDSP_1:def 15
for b1, b2 being Element of setvect a1 holds a2 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of setvect c1 st
for b2, b3 being Element of setvect c1 holds b1 . b2,b3 = b2 + b3
proof end;
uniqueness
for b1, b2 being BinOp of setvect c1 st ( for b3, b4 being Element of setvect c1 holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of setvect c1 holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines addvect MIDSP_1:def 15 :
for b1 being MidSp
for b2 being BinOp of setvect b1 holds
( b2 = addvect b1 iff for b3, b4 being Element of setvect b1 holds b2 . b3,b4 = b3 + b4 );

theorem Th76: :: MIDSP_1:76
canceled;

theorem Th77: :: MIDSP_1:77
for b1 being MidSp
for b2 being Element of setvect b1 ex b3 being Element of setvect b1 st b2 + b3 = ID b1
proof end;

theorem Th78: :: MIDSP_1:78
for b1 being MidSp
for b2, b3, b4 being Element of setvect b1 st b2 + b3 = ID b1 & b2 + b4 = ID b1 holds
b3 = b4
proof end;

definition
let c1 be MidSp;
func complvect c1 -> UnOp of setvect a1 means :Def16: :: MIDSP_1:def 16
for b1 being Element of setvect a1 holds b1 + (a2 . b1) = ID a1;
existence
ex b1 being UnOp of setvect c1 st
for b2 being Element of setvect c1 holds b2 + (b1 . b2) = ID c1
proof end;
uniqueness
for b1, b2 being UnOp of setvect c1 st ( for b3 being Element of setvect c1 holds b3 + (b1 . b3) = ID c1 ) & ( for b3 being Element of setvect c1 holds b3 + (b2 . b3) = ID c1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines complvect MIDSP_1:def 16 :
for b1 being MidSp
for b2 being UnOp of setvect b1 holds
( b2 = complvect b1 iff for b3 being Element of setvect b1 holds b3 + (b2 . b3) = ID b1 );

definition
let c1 be MidSp;
func zerovect c1 -> Element of setvect a1 equals :: MIDSP_1:def 17
 ID a1;
coherence
ID c1 is Element of setvect c1 by Th71;
end;

:: deftheorem Def17 defines zerovect MIDSP_1:def 17 :
for b1 being MidSp holds zerovect b1 = ID b1;

definition
let c1 be MidSp;
func vectgroup c1 -> LoopStr equals :: MIDSP_1:def 18
 LoopStr(# (setvect a1),(addvect a1),(zerovect a1) #);
coherence
LoopStr(# (setvect c1),(addvect c1),(zerovect c1) #) is LoopStr ;
end;

:: deftheorem Def18 defines vectgroup MIDSP_1:def 18 :
for b1 being MidSp holds vectgroup b1 = LoopStr(# (setvect b1),(addvect b1),(zerovect b1) #);

registration
let c1 be MidSp;
cluster vectgroup a1 -> non empty strict ;
coherence
( vectgroup c1 is strict & not vectgroup c1 is empty )
proof end;
end;

theorem Th79: :: MIDSP_1:79
canceled;

theorem Th80: :: MIDSP_1:80
canceled;

theorem Th81: :: MIDSP_1:81
canceled;

theorem Th82: :: MIDSP_1:82
for b1 being MidSp holds the carrier of (vectgroup b1) = setvect b1 ;

theorem Th83: :: MIDSP_1:83
for b1 being MidSp holds the add of (vectgroup b1) = addvect b1 ;

theorem Th84: :: MIDSP_1:84
canceled;

theorem Th85: :: MIDSP_1:85
for b1 being MidSp holds the Zero of (vectgroup b1) = zerovect b1 ;

theorem Th86: :: MIDSP_1:86
for b1 being MidSp holds
( vectgroup b1 is add-associative & vectgroup b1 is right_zeroed & vectgroup b1 is right_complementable & vectgroup b1 is Abelian )
proof end;