:: Reper Algebras
:: by Micha{\l} Muzalewski
::
:: Received May 28, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem :: MIDSP_3:1
for j, k being Element of NAT
for D being non empty set
for p being FinSequence of D st len p = (j + 1) + k holds
ex q, r being FinSequence of D ex c being Element of D st
( len q = j &amp; len r = k &amp; p = (q ^ <*c*>) ^ r )
proofend;

theorem :: MIDSP_3:2
for i, n being Element of NAT st i in Seg n holds
ex j, k being Element of NAT st
( n = (j + 1) + k &amp; i = j + 1 )
proofend;

theorem :: MIDSP_3:3
for i being Element of NAT
for D being non empty set
for c being Element of D
for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r &amp; i = (len q) + 1 holds
( ( for l being Element of NAT st 1 <= l &amp; l <= len q holds
p . l = q . l ) &amp; p . i = c &amp; ( for l being Element of NAT st i + 1 <= l &amp; l <= len p holds
p . l = r . (l - i) ) )
proofend;

theorem Th4: :: MIDSP_3:4
for l, j being Element of NAT holds
( l <= j or l = j + 1 or j + 2 <= l )
proofend;

theorem :: MIDSP_3:5
for l, n, i, j being Element of NAT st l in (Seg n) \ {i} &amp; i = j + 1 &amp; not ( 1 <= l &amp; l <= j ) holds
( i + 1 <= l &amp; l <= n )
proofend;

definition
let D be non empty set ;
let n be Element of NAT ;
let p be Element of n -tuples_on D;
let i be Element of NAT ;
let d be Element of D;
:: original:+*
redefine funcp +* (i,d) ->  Element of n -tuples_on D;
coherence
 p +* (i,d) is Element of n -tuples_on D
proofend;
end;

Lm1:  for n, i being Element of NAT
for D being non empty set
for d being Element of D
for p being Element of n -tuples_on D st i in Seg n holds
(p +* (i,d)) . i = d
proofend;

Lm2:  for n, i being Element of NAT
for D being non empty set
for d being Element of D
for p being Element of n -tuples_on D
for l being Element of NAT st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
proofend;

begin

definition
let n be Element of NAT ;
attrc2 is strict ;
struct ReperAlgebraStr over n ->  MidStr ;
aggrReperAlgebraStr(# carrier, MIDPOINT, reper #) ->  ReperAlgebraStr over n;
sel reper c2 ->  Function of (n -tuples_on the carrier of c2), the carrier of c2;
end;

registration
let n be Element of NAT ;
let A be non empty set ;
let m be BinOp of A;
let r be Function of (n -tuples_on A),A;
cluster ReperAlgebraStr(# A,m,r #) ->  non empty ;
coherence
 not ReperAlgebraStr(# A,m,r #) is empty ;
end;

Lm3: now__::_thesis:_for_n_being_Element_of_NAT_
for_M_being_MidSp
for_R_being_Function_of_((n_+_2)_-tuples_on_the_carrier_of_M),_the_carrier_of_M_holds_ReperAlgebraStr(#_the_carrier_of_M,_the_MIDPOINT_of_M,R_#)_is_MidSp-like
let n be Element of NAT ; ::_thesis: for M being MidSp
for R being Function of ((n + 2) -tuples_on the carrier of M), the carrier of M holds ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like
let M be MidSp; ::_thesis: for R being Function of ((n + 2) -tuples_on the carrier of M), the carrier of M holds ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like
let R be Function of ((n + 2) -tuples_on the carrier of M), the carrier of M; ::_thesis: ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like
set RA = ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #);
thus  ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) is MidSp-like ::_thesis: verum
proof
let a, b, c, d be Element of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #); :: according toMIDSP_1:def_3 ::_thesis: ( a @ a = a &amp; a @ b = b @ a &amp; (a @ b) @ (c @ d) = (a @ c) @ (b @ d) &amp; ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of M ;
thus a @ a = a9 @ a9
.= a by MIDSP_1:def_3 ; ::_thesis: ( a @ b = b @ a &amp; (a @ b) @ (c @ d) = (a @ c) @ (b @ d) &amp; ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b )
consider x9 being Element of M such that
A1: x9 @ a9 = b9 by MIDSP_1:def_3;
 for a, b being Element of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #)
for a9, b9 being Element of M st a = a9 &amp; b = b9 holds
a @ b = a9 @ b9 ;
hence a @ b = b9 @ a9
.= b @ a ;
::_thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) &amp; ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b )
reconsider x = x9 as Element of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) ;
thus (a @ b) @ (c @ d) = (a9 @ b9) @ (c9 @ d9)
.= (a9 @ c9) @ (b9 @ d9) by MIDSP_1:def_3
.= (a @ c) @ (b @ d) ; ::_thesis: ex b1 being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b1 @ a = b
take  x ; ::_thesis: x @ a = b
thus  x @ a = b by A1; ::_thesis: verum
end;
end;

registration
let n be Element of NAT ;
cluster non empty for ReperAlgebraStr over n;
existence
 not for b1 being ReperAlgebraStr over n holds b1 is empty
proofend;
end;

registration
let n be Element of NAT ;
cluster non empty MidSp-like for ReperAlgebraStr over n + 2;
existence
 ex b1 being non empty ReperAlgebraStr over n + 2 st b1 is MidSp-like
proofend;
end;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let i be Element of NAT ;
mode Tuple of i,RAS is Element of i -tuples_on the carrier of RAS;
end;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let a be Point of RAS;
:: original:<*
redefine func<*a*> ->  Tuple of 1,RAS;
coherence
 <*a*> is Tuple of 1,RAS by FINSEQ_2:98;
end;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let i, j be Element of NAT ;
let p be Tuple of i,RAS;
let q be Tuple of j,RAS;
:: original:^
redefine funcp ^ q ->  Tuple of (i + j),RAS;
coherence
 p ^ q is Tuple of (i + j),RAS
proofend;
end;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let a be Point of RAS;
let p be Tuple of (n + 1),RAS;
func *' (a,p) ->  Point of RAS equals :: MIDSP_3:def 1
 the reper of RAS . (<*a*> ^ p);
coherence
 the reper of RAS . (<*a*> ^ p) is Point of RAS
proofend;
end;

:: deftheorem  defines *' MIDSP_3:def_1_:_
 for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,p) = the reper of RAS . (<*a*> ^ p);

theorem :: MIDSP_3:6
for i, n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for d being Point of RAS
for p being Tuple of (n + 1),RAS st i in Seg (n + 1) holds
( (p +* (i,d)) . i = d &amp; ( for l being Element of NAT st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l ) ) by Lm1, Lm2;

definition
let n be Element of NAT ;
mode Nat of n ->  Element of NAT  means :Def2: :: MIDSP_3:def 2
( 1 <= it &amp; it <= n + 1 );
existence
 ex b1 being Element of NAT st
( 1 <= b1 &amp; b1 <= n + 1 )
proofend;
end;

:: deftheorem Def2 defines Nat MIDSP_3:def_2_:_
 for n, b2 being Element of NAT holds
( b2 is Nat of n iff ( 1 <= b2 &amp; b2 <= n + 1 ) );

theorem Th7: :: MIDSP_3:7
for i, n being Element of NAT holds
( i is Nat of n iff i in Seg (n + 1) )
proofend;

theorem Th8: :: MIDSP_3:8
for i, n being Element of NAT st i <= n holds
i + 1 is Nat of n
proofend;

theorem Th9: :: MIDSP_3:9
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds
p = q
proofend;

theorem Th10: :: MIDSP_3:10
for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for d being Point of RAS
for p being Tuple of (n + 1),RAS
for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
proofend;

definition
let n be Element of NAT ;
let D be non empty set ;
let p be Element of (n + 1) -tuples_on D;
let m be Nat of n;
:: original:.
redefine funcp . m ->  Element of D;
coherence
 p . m is Element of D
proofend;
end;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
attrRAS is being_invariance  means :Def3: :: MIDSP_3:def 3
 for a, b being Point of RAS
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p));
end;

:: deftheorem Def3 defines being_invariance MIDSP_3:def_3_:_
 for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS is being_invariance iff for a, b being Point of RAS
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p)) );

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let p be Tuple of (n + 1),RAS;
let i be Element of NAT ;
let a be Point of RAS;
:: original:+*
redefine funcp +* (i,a) ->  Tuple of (n + 1),RAS;
coherence
 p +* (i,a) is Tuple of (n + 1),RAS
proofend;
end;

definition
let n, i be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
predRAS has_property_of_zero_in i means :Def4: :: MIDSP_3:def 4
 for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (i,a))) = a;
end;

:: deftheorem Def4 defines has_property_of_zero_in MIDSP_3:def_4_:_
 for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS has_property_of_zero_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (i,a))) = a );

definition
let n, i be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
predRAS is_semi_additive_in i means :Def5: :: MIDSP_3:def 5
 for a, pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' (a,(p +* (i,(a @ pii)))) = a @ (*' (a,p));
end;

:: deftheorem Def5 defines is_semi_additive_in MIDSP_3:def_5_:_
 for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS is_semi_additive_in i iff for a, pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' (a,(p +* (i,(a @ pii)))) = a @ (*' (a,p)) );

theorem Th11: :: MIDSP_3:11
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for m being Nat of n st RAS is_semi_additive_in m holds
for a, d being Point of RAS
for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds
*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))
proofend;

definition
let n, i be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
predRAS is_additive_in i means :Def6: :: MIDSP_3:def 6
 for a, pii, p9i being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' (a,(p +* (i,(pii @ p9i)))) = (*' (a,p)) @ (*' (a,(p +* (i,p9i))));
end;

:: deftheorem Def6 defines is_additive_in MIDSP_3:def_6_:_
 for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS is_additive_in i iff for a, pii, p9i being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' (a,(p +* (i,(pii @ p9i)))) = (*' (a,p)) @ (*' (a,(p +* (i,p9i)))) );

definition
let n, i be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
predRAS is_alternative_in i means :Def7: :: MIDSP_3:def 7
 for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pii being Point of RAS st p . i = pii holds
*' (a,(p +* ((i + 1),pii))) = a;
end;

:: deftheorem Def7 defines is_alternative_in MIDSP_3:def_7_:_
 for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS is_alternative_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pii being Point of RAS st p . i = pii holds
*' (a,(p +* ((i + 1),pii))) = a );

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let W be ATLAS of RAS;
let i be Element of NAT ;
mode Tuple of i,W is Element of i -tuples_on the carrier of the algebra of W;
end;

theorem :: MIDSP_3:12
for i, n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st i in Seg (n + 1) holds
( (x +* (i,v)) . i = v &amp; ( for l being Element of NAT st l in (dom x) \ {i} holds
(x +* (i,v)) . l = x . l ) ) by Lm1, Lm2;

theorem Th13: :: MIDSP_3:13
for n, i being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W holds
( ( for l being Nat of n st l = i holds
(x +* (i,v)) . l = v ) &amp; ( for l, i being Nat of n st l <> i holds
(x +* (i,v)) . l = x . l ) )
proofend;

theorem Th14: :: MIDSP_3:14
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds
x = y
proofend;

scheme :: MIDSP_3:sch 1
SeqLambdaD9{ F1() ->  Element of NAT , F2() ->  non empty set , F3( set ) ->  Element of F2() } :
 ex z being FinSequence of F2() st
( len z = F1() + 1 &amp; ( for j being Nat of F1() holds z . j = F3(j) ) )
proofend;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let W be ATLAS of RAS;
let a be Point of RAS;
let x be Tuple of (n + 1),W;
func(a,x) . W ->  Tuple of (n + 1),RAS means :Def8: :: MIDSP_3:def 8
 for m being Nat of n holds it . m = (a,(x . m)) . W;
existence
 ex b1 being Tuple of (n + 1),RAS st
for m being Nat of n holds b1 . m = (a,(x . m)) . W
proofend;
uniqueness
 for b1, b2 being Tuple of (n + 1),RAS st ( for m being Nat of n holds b1 . m = (a,(x . m)) . W ) &amp; ( for m being Nat of n holds b2 . m = (a,(x . m)) . W ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines . MIDSP_3:def_8_:_
 for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for a being Point of RAS
for x being Tuple of (n + 1),W
for b6 being Tuple of (n + 1),RAS holds
( b6 = (a,x) . W iff for m being Nat of n holds b6 . m = (a,(x . m)) . W );

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let W be ATLAS of RAS;
let a be Point of RAS;
let p be Tuple of (n + 1),RAS;
funcW . (a,p) ->  Tuple of (n + 1),W means :Def9: :: MIDSP_3:def 9
 for m being Nat of n holds it . m = W . (a,(p . m));
existence
 ex b1 being Tuple of (n + 1),W st
for m being Nat of n holds b1 . m = W . (a,(p . m))
proofend;
uniqueness
 for b1, b2 being Tuple of (n + 1),W st ( for m being Nat of n holds b1 . m = W . (a,(p . m)) ) &amp; ( for m being Nat of n holds b2 . m = W . (a,(p . m)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines . MIDSP_3:def_9_:_
 for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for b6 being Tuple of (n + 1),W holds
( b6 = W . (a,p) iff for m being Nat of n holds b6 . m = W . (a,(p . m)) );

theorem Th15: :: MIDSP_3:15
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . (a,p) = x iff (a,x) . W = p )
proofend;

theorem :: MIDSP_3:16
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds W . (a,((a,x) . W)) = x by Th15;

theorem :: MIDSP_3:17
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS holds (a,(W . (a,p))) . W = p by Th15;

definition
let n be Element of NAT ;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let W be ATLAS of RAS;
let a be Point of RAS;
let x be Tuple of (n + 1),W;
func Phi (a,x) ->  Vector of W equals :: MIDSP_3:def 10
W . (a,(*' (a,((a,x) . W))));
coherence
 W . (a,(*' (a,((a,x) . W)))) is Vector of W ;
end;

:: deftheorem  defines Phi MIDSP_3:def_10_:_
 for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for a being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = W . (a,(*' (a,((a,x) . W))));

theorem Th18: :: MIDSP_3:18
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . (a,p) = x &amp; W . (a,b) = v holds
( *' (a,p) = b iff Phi (a,x) = v )
proofend;

theorem Th19: :: MIDSP_3:19
for n being Element of NAT
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS holds
( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
proofend;

theorem Th20: :: MIDSP_3:20
for n being Element of NAT holds 1 in Seg (n + 1)
proofend;

theorem Th21: :: MIDSP_3:21
for n being Element of NAT holds 1 is Nat of n
proofend;

begin

definition
let n be Element of NAT ;
mode ReperAlgebra of n ->  non empty MidSp-like ReperAlgebraStr over n + 2 means :Def11: :: MIDSP_3:def 11
it is being_invariance ;
existence
 ex b1 being non empty MidSp-like ReperAlgebraStr over n + 2 st b1 is being_invariance
proofend;
end;

:: deftheorem Def11 defines ReperAlgebra MIDSP_3:def_11_:_
 for n being Element of NAT
for b2 being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( b2 is ReperAlgebra of n iff b2 is being_invariance );

theorem Th22: :: MIDSP_3:22
for n being Element of NAT
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
proofend;

definition
let n be Element of NAT ;
let RAS be ReperAlgebra of n;
let W be ATLAS of RAS;
let x be Tuple of (n + 1),W;
func Phi x ->  Vector of W means :Def12: :: MIDSP_3:def 12
 for a being Point of RAS holds it = Phi (a,x);
existence
 ex b1 being Vector of W st
for a being Point of RAS holds b1 = Phi (a,x)
proofend;
uniqueness
 for b1, b2 being Vector of W st ( for a being Point of RAS holds b1 = Phi (a,x) ) &amp; ( for a being Point of RAS holds b2 = Phi (a,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines Phi MIDSP_3:def_12_:_
 for n being Element of NAT
for RAS being ReperAlgebra of n
for W being ATLAS of RAS
for x being Tuple of (n + 1),W
for b5 being Vector of W holds
( b5 = Phi x iff for a being Point of RAS holds b5 = Phi (a,x) );

Lm4:  for n being Element of NAT
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st W . (a,p) = x holds
Phi x = W . (a,(*' (a,p)))
proofend;

Lm5:  for n being Element of NAT
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
proofend;

theorem Th23: :: MIDSP_3:23
for n being Element of NAT
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . (a,p) = x &amp; W . (a,b) = v &amp; Phi x = v holds
*' (a,p) = b
proofend;

theorem Th24: :: MIDSP_3:24
for n being Element of NAT
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p &amp; (a,v) . W = b &amp; *' (a,p) = b holds
Phi x = v
proofend;

theorem Th25: :: MIDSP_3:25
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . (a,p) = x &amp; W . (a,b) = v holds
W . (a,(p +* (m,b))) = x +* (m,v)
proofend;

theorem Th26: :: MIDSP_3:26
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p &amp; (a,v) . W = b holds
(a,(x +* (m,v))) . W = p +* (m,b)
proofend;

theorem :: MIDSP_3:27
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W )
proofend;

theorem Th28: :: MIDSP_3:28
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) )
proofend;

theorem Th29: :: MIDSP_3:29
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n st RAS has_property_of_zero_in m &amp; RAS is_additive_in m holds
RAS is_semi_additive_in m
proofend;

Lm6:  for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS is_semi_additive_in m holds
for a, p9m, p99m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p99m = (p . m) @ p9m holds
( *' (a,(p +* (m,((p . m) @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) iff W . (a,(*' (a,(p +* (m,p99m))))) = (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m)))))) )
proofend;

Lm7:  for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st ( for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) holds
RAS is_semi_additive_in m
proofend;

theorem :: MIDSP_3:30
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )
proofend;

theorem Th31: :: MIDSP_3:31
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st W . (a,p) = x &amp; m <= n holds
W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m))
proofend;

theorem Th32: :: MIDSP_3:32
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p &amp; m <= n holds
(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))
proofend;

theorem :: MIDSP_3:33
for n being Element of NAT
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st m <= n holds
( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
proofend;