:: MIDSP_3 semantic presentation

theorem Th1: :: MIDSP_3:1
for b1, b2 being Nat
for b3 being non empty set
for b4 being FinSequence of b3 st len b4 = (b1 + 1) + b2 holds
ex b5, b6 being FinSequence of b3ex b7 being Element of b3 st
( len b5 = b1 & len b6 = b2 & b4 = (b5 ^ <*b7*>) ^ b6 )
proof end;

theorem Th2: :: MIDSP_3:2
for b1, b2 being Nat st b1 in Seg b2 holds
ex b3, b4 being Nat st
( b2 = (b3 + 1) + b4 & b1 = b3 + 1 )
proof end;

theorem Th3: :: MIDSP_3:3
for b1 being Nat
for b2 being non empty set
for b3 being Element of b2
for b4, b5, b6 being FinSequence of b2 st b4 = (b5 ^ <*b3*>) ^ b6 & b1 = (len b5) + 1 holds
( ( for b7 being Nat st 1 <= b7 & b7 <= len b5 holds
b4 . b7 = b5 . b7 ) & b4 . b1 = b3 & ( for b7 being Nat st b1 + 1 <= b7 & b7 <= len b4 holds
b4 . b7 = b6 . (b7 - b1) ) )
proof end;

theorem Th4: :: MIDSP_3:4
for b1, b2 being Nat holds
( b1 <= b2 or b1 = b2 + 1 or b2 + 2 <= b1 )
proof end;

theorem Th5: :: MIDSP_3:5
for b1, b2, b3, b4 being Nat st b1 in (Seg b2) \ {b3} & b3 = b4 + 1 & not ( 1 <= b1 & b1 <= b4 ) holds
( b3 + 1 <= b1 & b1 <= b2 )
proof end;

definition
let c1, c2 be Nat;
let c3 be non empty set ;
let c4 be Element of c3;
let c5 be Element of c1 -tuples_on c3;
assume E6: c2 in Seg c1 ;
func sub c5,c2,c4 -> Element of a1 -tuples_on a3 means :Def1: :: MIDSP_3:def 1
( a6 . a2 = a4 & ( for b1 being Nat st b1 in (dom a5) \ {a2} holds
a6 . b1 = a5 . b1 ) );
existence
ex b1 being Element of c1 -tuples_on c3 st
( b1 . c2 = c4 & ( for b2 being Nat st b2 in (dom c5) \ {c2} holds
b1 . b2 = c5 . b2 ) )
proof end;
uniqueness
for b1, b2 being Element of c1 -tuples_on c3 st b1 . c2 = c4 & ( for b3 being Nat st b3 in (dom c5) \ {c2} holds
b1 . b3 = c5 . b3 ) & b2 . c2 = c4 & ( for b3 being Nat st b3 in (dom c5) \ {c2} holds
b2 . b3 = c5 . b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines sub MIDSP_3:def 1 :
for b1, b2 being Nat
for b3 being non empty set
for b4 being Element of b3
for b5 being Element of b1 -tuples_on b3 st b2 in Seg b1 holds
for b6 being Element of b1 -tuples_on b3 holds
( b6 = sub b5,b2,b4 iff ( b6 . b2 = b4 & ( for b7 being Nat st b7 in (dom b5) \ {b2} holds
b6 . b7 = b5 . b7 ) ) );

definition
let c1 be Nat;
attr a2 is strict;
struct ReperAlgebraStr of c1 -> MidStr ;
aggr ReperAlgebraStr(# carrier, MIDPOINT, reper #) -> ReperAlgebraStr of a1;
sel reper c2 -> Function of a1 -tuples_on the carrier of a2,the carrier of a2;
end;

registration
let c1 be Nat;
let c2 be non empty set ;
let c3 be BinOp of c2;
let c4 be Function of c1 -tuples_on c2,c2;
cluster ReperAlgebraStr(# a2,a3,a4 #) -> non empty ;
coherence
not ReperAlgebraStr(# c2,c3,c4 #) is empty by STRUCT_0:def 1;
end;

E7: now
let c1 be Nat;
let c2 be MidSp;
let c3 be Function of (c1 + 2) -tuples_on the carrier of c2,the carrier of c2;
set c4 = ReperAlgebraStr(# the carrier of c2,the MIDPOINT of c2,c3 #);
thus ReperAlgebraStr(# the carrier of c2,the MIDPOINT of c2,c3 #) is MidSp-like
proof
let c5, c6, c7, c8 be Element of ReperAlgebraStr(# the carrier of c2,the MIDPOINT of c2,c3 #); :: according to MIDSP_1:def 4
reconsider c9 = c5, c10 = c6, c11 = c7, c12 = c8 as Element of c2 ;
E8: for b1, b2 being Element of ReperAlgebraStr(# the carrier of c2,the MIDPOINT of c2,c3 #)
for b3, b4 being Element of c2 st b1 = b3 & b2 = b4 holds
b1 @ b2 = b3 @ b4 ;
thus c5 @ c5 = c9 @ c9
.= c5 by MIDSP_1:def 4 ;
thus c5 @ c6 = c10 @ c9 by E8
.= c6 @ c5 ;
( c5 @ c6 = c9 @ c10 & c7 @ c8 = c11 @ c12 & c9 @ c11 = c5 @ c7 & c10 @ c12 = c6 @ c8 ) by E8;
hence (c5 @ c6) @ (c7 @ c8) = (c9 @ c10) @ (c11 @ c12)
.= (c9 @ c11) @ (c10 @ c12) by MIDSP_1:def 4
.= (c5 @ c7) @ (c6 @ c8) ;

consider c13 being Element of c2 such that
E9: c13 @ c9 = c10 by MIDSP_1:def 4;
reconsider c14 = c13 as Element of ReperAlgebraStr(# the carrier of c2,the MIDPOINT of c2,c3 #) ;
take c14 ;
thus c14 @ c5 = c6 by E9;
end;
end;

registration
let c1 be Nat;
cluster non empty ReperAlgebraStr of a1;
existence
not for b1 being ReperAlgebraStr of c1 holds b1 is empty
proof end;
end;

registration
let c1 be Nat;
cluster non empty MidSp-like ReperAlgebraStr of a1 + 2;
existence
ex b1 being non empty ReperAlgebraStr of c1 + 2 st b1 is MidSp-like
proof end;
end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be Nat;
mode Tuple of a3,a2 is Tuple of a3,the carrier of a2;
end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be Point of c2;
redefine func <* as <*c3*> -> Tuple of 1,a2;
coherence
<*c3*> is Tuple of 1,c2 by FINSEQ_2:118;
end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3, c4 be Nat;
let c5 be Tuple of c3,c2;
let c6 be Tuple of c4,c2;
redefine func ^ as c5 ^ c6 -> Tuple of (a3 + a4),a2;
coherence
c5 ^ c6 is Tuple of (c3 + c4),c2 by FINSEQ_2:127;
end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be Point of c2;
let c4 be Tuple of (c1 + 1),c2;
func *' c3,c4 -> Point of a2 equals :: MIDSP_3:def 2
the reper of a2 . (<*a3*> ^ a4);
coherence
the reper of c2 . (<*c3*> ^ c4) is Point of c2
proof end;
end;

:: deftheorem Def2 defines *' MIDSP_3:def 2 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being Point of b2
for b4 being Tuple of (b1 + 1),b2 holds *' b3,b4 = the reper of b2 . (<*b3*> ^ b4);

definition
let c1, c2 be Nat;
let c3 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c4 be Point of c3;
let c5 be Tuple of (c1 + 1),c3;
func <:c5,c2,c4:> -> Tuple of (a1 + 1),a3 means :Def3: :: MIDSP_3:def 3
for b1 being non empty set
for b2 being Element of (a1 + 1) -tuples_on b1
for b3 being Element of b1 st b1 = the carrier of a3 & b2 = a5 & b3 = a4 holds
a6 = sub b2,a2,b3;
existence
ex b1 being Tuple of (c1 + 1),c3 st
for b2 being non empty set
for b3 being Element of (c1 + 1) -tuples_on b2
for b4 being Element of b2 st b2 = the carrier of c3 & b3 = c5 & b4 = c4 holds
b1 = sub b3,c2,b4
proof end;
uniqueness
for b1, b2 being Tuple of (c1 + 1),c3 st ( for b3 being non empty set
for b4 being Element of (c1 + 1) -tuples_on b3
for b5 being Element of b3 st b3 = the carrier of c3 & b4 = c5 & b5 = c4 holds
b1 = sub b4,c2,b5 ) & ( for b3 being non empty set
for b4 being Element of (c1 + 1) -tuples_on b3
for b5 being Element of b3 st b3 = the carrier of c3 & b4 = c5 & b5 = c4 holds
b2 = sub b4,c2,b5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines <: MIDSP_3:def 3 :
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b4 being Point of b3
for b5, b6 being Tuple of (b1 + 1),b3 holds
( b6 = <:b5,b2,b4:> iff for b7 being non empty set
for b8 being Element of (b1 + 1) -tuples_on b7
for b9 being Element of b7 st b7 = the carrier of b3 & b8 = b5 & b9 = b4 holds
b6 = sub b8,b2,b9 );

theorem Th6: :: MIDSP_3:6
canceled;

theorem Th7: :: MIDSP_3:7
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b2 + 2
for b4 being Point of b3
for b5 being Tuple of (b2 + 1),b3 st b1 in Seg (b2 + 1) holds
( <:b5,b1,b4:> . b1 = b4 & ( for b6 being Nat st b6 in (dom b5) \ {b1} holds
<:b5,b1,b4:> . b6 = b5 . b6 ) )
proof end;

definition
let c1 be Nat;
mode Nat of c1 -> Nat means :Def4: :: MIDSP_3:def 4
( 1 <= a2 & a2 <= a1 + 1 );
existence
ex b1 being Nat st
( 1 <= b1 & b1 <= c1 + 1 )
proof end;
end;

:: deftheorem Def4 defines Nat MIDSP_3:def 4 :
for b1, b2 being Nat holds
( b2 is Nat of b1 iff ( 1 <= b2 & b2 <= b1 + 1 ) );

theorem Th8: :: MIDSP_3:8
for b1, b2 being Nat holds
( b1 is Nat of b2 iff b1 in Seg (b2 + 1) )
proof end;

theorem Th9: :: MIDSP_3:9
canceled;

theorem Th10: :: MIDSP_3:10
for b1, b2 being Nat st b1 <= b2 holds
b1 + 1 is Nat of b2
proof end;

theorem Th11: :: MIDSP_3:11
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3, b4 being Tuple of (b1 + 1),b2 st ( for b5 being Nat of b1 holds b3 . b5 = b4 . b5 ) holds
b3 = b4
proof end;

theorem Th12: :: MIDSP_3:12
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b4 being Point of b3
for b5 being Tuple of (b1 + 1),b3 holds
( ( for b6 being Nat of b1 st b6 = b2 holds
<:b5,b2,b4:> . b6 = b4 ) & ( for b6, b7 being Nat of b1 st b6 <> b7 holds
<:b5,b7,b4:> . b6 = b5 . b6 ) )
proof end;

definition
let c1 be Nat;
let c2 be non empty set ;
let c3 be Element of (c1 + 1) -tuples_on c2;
let c4 be Nat of c1;
redefine func . as c3 . c4 -> Element of a2;
coherence
c3 . c4 is Element of c2
proof end;
end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
attr a2 is being_invariance means :Def5: :: MIDSP_3:def 5
for b1, b2 being Point of a2
for b3, b4 being Tuple of (a1 + 1),a2 st ( for b5 being Nat of a1 holds b1 @ (b4 . b5) = b2 @ (b3 . b5) ) holds
b1 @ (*' b2,b4) = b2 @ (*' b1,b3);
end;

:: deftheorem Def5 defines being_invariance MIDSP_3:def 5 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2 holds
( b2 is being_invariance iff for b3, b4 being Point of b2
for b5, b6 being Tuple of (b1 + 1),b2 st ( for b7 being Nat of b1 holds b3 @ (b6 . b7) = b4 @ (b5 . b7) ) holds
b3 @ (*' b4,b6) = b4 @ (*' b3,b5) );

notation
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
synonym c2 is_invariance for being_invariance c2;
end;

definition
let c1, c2 be Nat;
let c3 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
pred c3 has_property_of_zero_in c2 means :Def6: :: MIDSP_3:def 6
for b1 being Point of a3
for b2 being Tuple of (a1 + 1),a3 holds *' b1,<:b2,a2,b1:> = b1;
end;

:: deftheorem Def6 defines has_property_of_zero_in MIDSP_3:def 6 :
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2 holds
( b3 has_property_of_zero_in b2 iff for b4 being Point of b3
for b5 being Tuple of (b1 + 1),b3 holds *' b4,<:b5,b2,b4:> = b4 );

definition
let c1, c2 be Nat;
let c3 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
pred c3 is_semi_additive_in c2 means :Def7: :: MIDSP_3:def 7
for b1, b2 being Point of a3
for b3 being Tuple of (a1 + 1),a3 st b3 . a2 = b2 holds
*' b1,<:b3,a2,(b1 @ b2):> = b1 @ (*' b1,b3);
end;

:: deftheorem Def7 defines is_semi_additive_in MIDSP_3:def 7 :
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2 holds
( b3 is_semi_additive_in b2 iff for b4, b5 being Point of b3
for b6 being Tuple of (b1 + 1),b3 st b6 . b2 = b5 holds
*' b4,<:b6,b2,(b4 @ b5):> = b4 @ (*' b4,b6) );

theorem Th13: :: MIDSP_3:13
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being Nat of b1 st b2 is_semi_additive_in b3 holds
for b4, b5 being Point of b2
for b6, b7 being Tuple of (b1 + 1),b2 st b7 = <:b6,b3,b5:> holds
*' b4,<:b6,b3,(b4 @ b5):> = b4 @ (*' b4,b7)
proof end;

definition
let c1, c2 be Nat;
let c3 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
pred c3 is_additive_in c2 means :Def8: :: MIDSP_3:def 8
for b1, b2, b3 being Point of a3
for b4 being Tuple of (a1 + 1),a3 st b4 . a2 = b2 holds
*' b1,<:b4,a2,(b2 @ b3):> = (*' b1,b4) @ (*' b1,<:b4,a2,b3:>);
end;

:: deftheorem Def8 defines is_additive_in MIDSP_3:def 8 :
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2 holds
( b3 is_additive_in b2 iff for b4, b5, b6 being Point of b3
for b7 being Tuple of (b1 + 1),b3 st b7 . b2 = b5 holds
*' b4,<:b7,b2,(b5 @ b6):> = (*' b4,b7) @ (*' b4,<:b7,b2,b6:>) );

definition
let c1, c2 be Nat;
let c3 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
pred c3 is_alternative_in c2 means :Def9: :: MIDSP_3:def 9
for b1 being Point of a3
for b2 being Tuple of (a1 + 1),a3
for b3 being Point of a3 st b2 . a2 = b3 holds
*' b1,<:b2,(a2 + 1),b3:> = b1;
end;

:: deftheorem Def9 defines is_alternative_in MIDSP_3:def 9 :
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2 holds
( b3 is_alternative_in b2 iff for b4 being Point of b3
for b5 being Tuple of (b1 + 1),b3
for b6 being Point of b3 st b5 . b2 = b6 holds
*' b4,<:b5,(b2 + 1),b6:> = b4 );

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be ATLAS of c2;
let c4 be Nat;
mode Tuple of a4,a3 is Tuple of a4,the carrier of the algebra of a3;
end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be ATLAS of c2;
let c4 be Tuple of (c1 + 1),c3;
let c5 be Nat;
let c6 be Vector of c3;
func <:c4,c5,c6:> -> Tuple of (a1 + 1),a3 means :Def10: :: MIDSP_3:def 10
for b1 being non empty set
for b2 being Element of (a1 + 1) -tuples_on b1
for b3 being Element of b1 st b1 = the carrier of the algebra of a3 & b2 = a4 & b3 = a6 holds
a7 = sub b2,a5,b3;
existence
ex b1 being Tuple of (c1 + 1),c3 st
for b2 being non empty set
for b3 being Element of (c1 + 1) -tuples_on b2
for b4 being Element of b2 st b2 = the carrier of the algebra of c3 & b3 = c4 & b4 = c6 holds
b1 = sub b3,c5,b4
proof end;
uniqueness
for b1, b2 being Tuple of (c1 + 1),c3 st ( for b3 being non empty set
for b4 being Element of (c1 + 1) -tuples_on b3
for b5 being Element of b3 st b3 = the carrier of the algebra of c3 & b4 = c4 & b5 = c6 holds
b1 = sub b4,c5,b5 ) & ( for b3 being non empty set
for b4 being Element of (c1 + 1) -tuples_on b3
for b5 being Element of b3 st b3 = the carrier of the algebra of c3 & b4 = c4 & b5 = c6 holds
b2 = sub b4,c5,b5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines <: MIDSP_3:def 10 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being ATLAS of b2
for b4 being Tuple of (b1 + 1),b3
for b5 being Nat
for b6 being Vector of b3
for b7 being Tuple of (b1 + 1),b3 holds
( b7 = <:b4,b5,b6:> iff for b8 being non empty set
for b9 being Element of (b1 + 1) -tuples_on b8
for b10 being Element of b8 st b8 = the carrier of the algebra of b3 & b9 = b4 & b10 = b6 holds
b7 = sub b9,b5,b10 );

theorem Th14: :: MIDSP_3:14
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b2 + 2
for b4 being ATLAS of b3
for b5 being Vector of b4
for b6 being Tuple of (b2 + 1),b4 st b1 in Seg (b2 + 1) holds
( <:b6,b1,b5:> . b1 = b5 & ( for b7 being Nat st b7 in (dom b6) \ {b1} holds
<:b6,b1,b5:> . b7 = b6 . b7 ) )
proof end;

theorem Th15: :: MIDSP_3:15
for b1, b2 being Nat
for b3 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b4 being ATLAS of b3
for b5 being Vector of b4
for b6 being Tuple of (b1 + 1),b4 holds
( ( for b7 being Nat of b1 st b7 = b2 holds
<:b6,b2,b5:> . b7 = b5 ) & ( for b7, b8 being Nat of b1 st b7 <> b8 holds
<:b6,b8,b5:> . b7 = b6 . b7 ) )
proof end;

theorem Th16: :: MIDSP_3:16
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being ATLAS of b2
for b4, b5 being Tuple of (b1 + 1),b3 st ( for b6 being Nat of b1 holds b4 . b6 = b5 . b6 ) holds
b4 = b5
proof end;

scheme :: MIDSP_3:sch 1
s1{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
ex b1 being FinSequence of F2() st
( len b1 = F1() + 1 & ( for b2 being Nat of F1() holds b1 . b2 = F3(b2) ) )
proof end;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be ATLAS of c2;
let c4 be Point of c2;
let c5 be Tuple of (c1 + 1),c3;
func c4,c5 . c3 -> Tuple of (a1 + 1),a2 means :Def11: :: MIDSP_3:def 11
for b1 being Nat of a1 holds a6 . b1 = a4,(a5 . b1) . a3;
existence
ex b1 being Tuple of (c1 + 1),c2 st
for b2 being Nat of c1 holds b1 . b2 = c4,(c5 . b2) . c3
proof end;
uniqueness
for b1, b2 being Tuple of (c1 + 1),c2 st ( for b3 being Nat of c1 holds b1 . b3 = c4,(c5 . b3) . c3 ) & ( for b3 being Nat of c1 holds b2 . b3 = c4,(c5 . b3) . c3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines . MIDSP_3:def 11 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being ATLAS of b2
for b4 being Point of b2
for b5 being Tuple of (b1 + 1),b3
for b6 being Tuple of (b1 + 1),b2 holds
( b6 = b4,b5 . b3 iff for b7 being Nat of b1 holds b6 . b7 = b4,(b5 . b7) . b3 );

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be ATLAS of c2;
let c4 be Point of c2;
let c5 be Tuple of (c1 + 1),c2;
func c3 . c4,c5 -> Tuple of (a1 + 1),a3 means :Def12: :: MIDSP_3:def 12
for b1 being Nat of a1 holds a6 . b1 = a3 . a4,(a5 . b1);
existence
ex b1 being Tuple of (c1 + 1),c3 st
for b2 being Nat of c1 holds b1 . b2 = c3 . c4,(c5 . b2)
proof end;
uniqueness
for b1, b2 being Tuple of (c1 + 1),c3 st ( for b3 being Nat of c1 holds b1 . b3 = c3 . c4,(c5 . b3) ) & ( for b3 being Nat of c1 holds b2 . b3 = c3 . c4,(c5 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines . MIDSP_3:def 12 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being ATLAS of b2
for b4 being Point of b2
for b5 being Tuple of (b1 + 1),b2
for b6 being Tuple of (b1 + 1),b3 holds
( b6 = b3 . b4,b5 iff for b7 being Nat of b1 holds b6 . b7 = b3 . b4,(b5 . b7) );

theorem Th17: :: MIDSP_3:17
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being Point of b2
for b4 being Tuple of (b1 + 1),b2
for b5 being ATLAS of b2
for b6 being Tuple of (b1 + 1),b5 holds
( b5 . b3,b4 = b6 iff b3,b6 . b5 = b4 )
proof end;

theorem Th18: :: MIDSP_3:18
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being Point of b2
for b4 being ATLAS of b2
for b5 being Tuple of (b1 + 1),b4 holds b4 . b3,(b3,b5 . b4) = b5 by Th17;

theorem Th19: :: MIDSP_3:19
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being Point of b2
for b4 being Tuple of (b1 + 1),b2
for b5 being ATLAS of b2 holds b3,(b5 . b3,b4) . b5 = b4 by Th17;

definition
let c1 be Nat;
let c2 be non empty MidSp-like ReperAlgebraStr of c1 + 2;
let c3 be ATLAS of c2;
let c4 be Point of c2;
let c5 be Tuple of (c1 + 1),c3;
func Phi c4,c5 -> Vector of a3 equals :: MIDSP_3:def 13
a3 . a4,(*' a4,(a4,a5 . a3));
coherence
c3 . c4,(*' c4,(c4,c5 . c3)) is Vector of c3 ;
end;

:: deftheorem Def13 defines Phi MIDSP_3:def 13 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being ATLAS of b2
for b4 being Point of b2
for b5 being Tuple of (b1 + 1),b3 holds Phi b4,b5 = b3 . b4,(*' b4,(b4,b5 . b3));

theorem Th20: :: MIDSP_3:20
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3, b4 being Point of b2
for b5 being Tuple of (b1 + 1),b2
for b6 being ATLAS of b2
for b7 being Vector of b6
for b8 being Tuple of (b1 + 1),b6 st b6 . b3,b5 = b8 & b6 . b3,b4 = b7 holds
( *' b3,b5 = b4 iff Phi b3,b8 = b7 )
proof end;

theorem Th21: :: MIDSP_3:21
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2
for b3 being ATLAS of b2 holds
( b2 is_invariance iff for b4, b5 being Point of b2
for b6 being Tuple of (b1 + 1),b3 holds Phi b4,b6 = Phi b5,b6 )
proof end;

theorem Th22: :: MIDSP_3:22
for b1 being Nat holds 1 in Seg (b1 + 1)
proof end;

theorem Th23: :: MIDSP_3:23
canceled;

theorem Th24: :: MIDSP_3:24
for b1 being Nat holds 1 is Nat of b1
proof end;

definition
let c1 be Nat;
mode ReperAlgebra of c1 -> non empty MidSp-like ReperAlgebraStr of a1 + 2 means :Def14: :: MIDSP_3:def 14
a2 is_invariance ;
existence
ex b1 being non empty MidSp-like ReperAlgebraStr of c1 + 2 st b1 is_invariance
proof end;
end;

:: deftheorem Def14 defines ReperAlgebra MIDSP_3:def 14 :
for b1 being Nat
for b2 being non empty MidSp-like ReperAlgebraStr of b1 + 2 holds
( b2 is ReperAlgebra of b1 iff b2 is_invariance );

theorem Th25: :: MIDSP_3:25
for b1 being Nat
for b2 being ReperAlgebra of b1
for b3, b4 being Point of b2
for b5 being ATLAS of b2
for b6 being Tuple of (b1 + 1),b5 holds Phi b3,b6 = Phi b4,b6
proof end;

definition
let c1 be Nat;
let c2 be ReperAlgebra of c1;
let c3 be ATLAS of c2;
let c4 be Tuple of (c1 + 1),c3;
func Phi c4 -> Vector of a3 means :Def15: :: MIDSP_3:def 15
for b1 being Point of a2 holds a5 = Phi b1,a4;
existence
ex b1 being Vector of c3 st
for b2 being Point of c2 holds b1 = Phi b2,c4
proof end;
uniqueness
for b1, b2 being Vector of c3 st ( for b3 being Point of c2 holds b1 = Phi b3,c4 ) & ( for b3 being Point of c2 holds b2 = Phi b3,c4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Phi MIDSP_3:def 15 :
for b1 being Nat
for b2 being ReperAlgebra of b1
for b3 being ATLAS of b2
for b4 being Tuple of (b1 + 1),b3
for b5 being Vector of b3 holds
( b5 = Phi b4 iff for b6 being Point of b2 holds b5 = Phi b6,b4 );

Lemma35: for b1 being Nat
for b2 being ReperAlgebra of b1
for b3 being Point of b2
for b4 being Tuple of (b1 + 1),b2
for b5 being ATLAS of b2
for b6 being Tuple of (b1 + 1),b5 st b5 . b3,b4 = b6 holds
Phi b6 = b5 . b3,(*' b3,b4)
proof end;

Lemma36: for b1 being Nat
for b2 being ReperAlgebra of b1
for b3 being Point of b2
for b4 being Tuple of (b1 + 1),b2
for b5 being ATLAS of b2
for b6 being Tuple of (b1 + 1),b5 st b3,b6 . b5 = b4 holds
Phi b6 = b5 . b3,(*' b3,b4)
proof end;

theorem Th26: :: MIDSP_3:26
for b1 being Nat
for b2 being ReperAlgebra of b1
for b3, b4 being Point of b2
for b5 being Tuple of (b1 + 1),b2
for b6 being ATLAS of b2
for b7 being Vector of b6
for b8 being Tuple of (b1 + 1),b6 st b6 . b3,b5 = b8 & b6 . b3,b4 = b7 & Phi b8 = b7 holds
*' b3,b5 = b4
proof end;

theorem Th27: :: MIDSP_3:27
for b1 being Nat
for b2 being ReperAlgebra of b1
for b3, b4 being Point of b2
for b5 being Tuple of (b1 + 1),b2
for b6 being ATLAS of b2
for b7 being Vector of b6
for b8 being Tuple of (b1 + 1),b6 st b3,b8 . b6 = b5 & b3,b7 . b6 = b4 & *' b3,b5 = b4 holds
Phi b8 = b7
proof end;

theorem Th28: :: MIDSP_3:28
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4, b5 being Point of b3
for b6 being Tuple of (b1 + 1),b3
for b7 being ATLAS of b3
for b8 being Vector of b7
for b9 being Tuple of (b1 + 1),b7 st b7 . b4,b6 = b9 & b7 . b4,b5 = b8 holds
b7 . b4,<:b6,b2,b5:> = <:b9,b2,b8:>
proof end;

theorem Th29: :: MIDSP_3:29
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4, b5 being Point of b3
for b6 being Tuple of (b1 + 1),b3
for b7 being ATLAS of b3
for b8 being Vector of b7
for b9 being Tuple of (b1 + 1),b7 st b4,b9 . b7 = b6 & b4,b8 . b7 = b5 holds
b4,<:b9,b2,b8:> . b7 = <:b6,b2,b5:>
proof end;

theorem Th30: :: MIDSP_3:30
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being ATLAS of b3 holds
( b3 has_property_of_zero_in b2 iff for b5 being Tuple of (b1 + 1),b4 holds Phi <:b5,b2,(0. b4):> = 0. b4 )
proof end;

theorem Th31: :: MIDSP_3:31
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being ATLAS of b3 holds
( b3 is_semi_additive_in b2 iff for b5 being Tuple of (b1 + 1),b4 holds Phi <:b5,b2,(Double (b5 . b2)):> = Double (Phi b5) )
proof end;

theorem Th32: :: MIDSP_3:32
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1 st b3 has_property_of_zero_in b2 & b3 is_additive_in b2 holds
b3 is_semi_additive_in b2
proof end;

Lemma43: for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being ATLAS of b3 st b3 is_semi_additive_in b2 holds
for b5, b6, b7 being Point of b3
for b8 being Tuple of (b1 + 1),b3 st b5 @ b7 = (b8 . b2) @ b6 holds
( *' b5,<:b8,b2,((b8 . b2) @ b6):> = (*' b5,b8) @ (*' b5,<:b8,b2,b6:>) iff b4 . b5,(*' b5,<:b8,b2,b7:>) = (b4 . b5,(*' b5,b8)) + (b4 . b5,(*' b5,<:b8,b2,b6:>)) )
proof end;

Lemma44: for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being ATLAS of b3 st ( for b5 being Tuple of (b1 + 1),b4
for b6 being Vector of b4 holds Phi <:b5,b2,((b5 . b2) + b6):> = (Phi b5) + (Phi <:b5,b2,b6:>) ) holds
b3 is_semi_additive_in b2
proof end;

theorem Th33: :: MIDSP_3:33
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being ATLAS of b3 st b3 has_property_of_zero_in b2 holds
( b3 is_additive_in b2 iff for b5 being Tuple of (b1 + 1),b4
for b6 being Vector of b4 holds Phi <:b5,b2,((b5 . b2) + b6):> = (Phi b5) + (Phi <:b5,b2,b6:>) )
proof end;

theorem Th34: :: MIDSP_3:34
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being Point of b3
for b5 being Tuple of (b1 + 1),b3
for b6 being ATLAS of b3
for b7 being Tuple of (b1 + 1),b6 st b6 . b4,b5 = b7 & b2 <= b1 holds
b6 . b4,<:b5,(b2 + 1),(b5 . b2):> = <:b7,(b2 + 1),(b7 . b2):>
proof end;

theorem Th35: :: MIDSP_3:35
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being Point of b3
for b5 being Tuple of (b1 + 1),b3
for b6 being ATLAS of b3
for b7 being Tuple of (b1 + 1),b6 st b4,b7 . b6 = b5 & b2 <= b1 holds
b4,<:b7,(b2 + 1),(b7 . b2):> . b6 = <:b5,(b2 + 1),(b5 . b2):>
proof end;

theorem Th36: :: MIDSP_3:36
for b1 being Nat
for b2 being Nat of b1
for b3 being ReperAlgebra of b1
for b4 being ATLAS of b3 st b2 <= b1 holds
( b3 is_alternative_in b2 iff for b5 being Tuple of (b1 + 1),b4 holds Phi <:b5,(b2 + 1),(b5 . b2):> = 0. b4 )
proof end;