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

theorem :: MIDSP_3:1
for j, k being 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 & len r = k & p = (q ^ <*c*>) ^ r )
proof end;

theorem :: MIDSP_3:2
for n, i being Nat st i in Seg n holds
ex j, k being Nat st
( n = (j + 1) + k & i = j + 1 )
proof end;

theorem :: MIDSP_3:3
for i being 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 & i = (len q) + 1 holds
( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
proof end;

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

theorem :: MIDSP_3:5
for n, i, j, l being Nat st l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) holds
( i + 1 <= l & l <= n )
proof end;

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

Lm1: for n, i being 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

proof end;

Lm2: for n, i being 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 Nat st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l

proof end;

definition
let n be Nat;
attr c2 is strict ;
struct ReperAlgebraStr over n -> MidStr ;
aggr ReperAlgebraStr(# 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 Nat;
let A be non empty set ;
let m be BinOp of A;
let r be Function of (),A;
cluster ReperAlgebraStr(# A,m,r #) -> non empty ;
coherence
not ReperAlgebraStr(# A,m,r #) is empty
;
end;

Lm3: now :: thesis: for n being 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 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 to MIDSP_1:def 3 :: thesis: ( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & 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 & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & 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 & b = b9 holds
a @ b = a9 @ b9 ;
hence a @ b = b9 @ a9
.= b @ a ;
:: thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & 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 Nat;
cluster non empty for ReperAlgebraStr over n;
existence
not for b1 being ReperAlgebraStr over n holds b1 is empty
proof end;
end;

registration
let n be 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
proof end;
end;

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

definition
let n be 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 Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let i, j be Nat;
let p be Tuple of i,RAS;
let q be Tuple of j,RAS;
:: original: ^
redefine func p ^ q -> Tuple of (i + j),RAS;
coherence
p ^ q is Tuple of (i + j),RAS
proof end;
end;

definition
let n be 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
proof end;
end;

:: deftheorem defines *' MIDSP_3:def 1 :
for n being 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 n, i being 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 & ( for l being Nat st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l ) ) by ;

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

:: deftheorem Def2 defines Nat MIDSP_3:def 2 :
for n, b2 being Nat holds
( b2 is Nat of n iff ( 1 <= b2 & b2 <= n + 1 ) );

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

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

theorem Th9: :: MIDSP_3:9
for n being 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
proof end;

theorem Th10: :: MIDSP_3:10
for n, i being 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
proof end;

definition
let n be 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 func p . m -> Element of D;
coherence
p . m is Element of D
proof end;
end;

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
attr RAS is being_invariance means :: 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 defines being_invariance MIDSP_3:def 3 :
for n being 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 Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let p be Tuple of (n + 1),RAS;
let i be Nat;
let a be Point of RAS;
:: original: +*
redefine func p +* (i,a) -> Tuple of (n + 1),RAS;
coherence
p +* (i,a) is Tuple of (n + 1),RAS
proof end;
end;

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
pred RAS has_property_of_zero_in i means :: 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 defines has_property_of_zero_in MIDSP_3:def 4 :
for n, i being 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 Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
pred RAS is_semi_additive_in i means :: 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 defines is_semi_additive_in MIDSP_3:def 5 :
for n, i being 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 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))
proof end;

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
pred RAS is_additive_in i means :: 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 defines is_additive_in MIDSP_3:def 6 :
for n, i being 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 Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
pred RAS is_alternative_in i means :: 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 defines is_alternative_in MIDSP_3:def 7 :
for n, i being 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 Nat;
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2;
let W be ATLAS of RAS;
let i be 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 n, i being 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 & ( for l being Nat st l in (dom x) \ {i} holds
(x +* (i,v)) . l = x . l ) ) by ;

theorem Th13: :: MIDSP_3:13
for n, i being 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 ) & ( for l, i being Nat of n st l <> i holds
(x +* (i,v)) . l = x . l ) )
proof end;

theorem Th14: :: MIDSP_3:14
for n being 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
proof end;

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

definition
let n be 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
proof end;
uniqueness
for b1, b2 being Tuple of (n + 1),RAS st ( for m being Nat of n holds b1 . m = (a,(x . m)) . W ) & ( for m being Nat of n holds b2 . m = (a,(x . m)) . W ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines . MIDSP_3:def 8 :
for n being 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 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;
func W . (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))
proof end;
uniqueness
for b1, b2 being Tuple of (n + 1),W st ( for m being Nat of n holds b1 . m = W . (a,(p . m)) ) & ( for m being Nat of n holds b2 . m = W . (a,(p . m)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines . MIDSP_3:def 9 :
for n being 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 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 )
proof end;

theorem :: MIDSP_3:16
for n being 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 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 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 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 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 & W . (a,b) = v holds
( *' (a,p) = b iff Phi (a,x) = v )
proof end;

theorem Th19: :: MIDSP_3:19
for n being 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) )
proof end;

theorem Th20: :: MIDSP_3:20
for n being Nat holds 1 in Seg (n + 1)
proof end;

theorem Th21: :: MIDSP_3:21
for n being Nat holds 1 is Nat of n
proof end;

definition
let n be 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
proof end;
end;

:: deftheorem Def11 defines ReperAlgebra MIDSP_3:def 11 :
for n being 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 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) by ;

definition
let n be 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)
proof end;
uniqueness
for b1, b2 being Vector of W st ( for a being Point of RAS holds b1 = Phi (a,x) ) & ( for a being Point of RAS holds b2 = Phi (a,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Phi MIDSP_3:def 12 :
for n being 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 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)))

proof end;

Lm5: for n being 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)))

proof end;

theorem Th23: :: MIDSP_3:23
for n being 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 & W . (a,b) = v & Phi x = v holds
*' (a,p) = b
proof end;

theorem Th24: :: MIDSP_3:24
for n being 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 & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
proof end;

theorem Th25: :: MIDSP_3:25
for n being 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 & W . (a,b) = v holds
W . (a,(p +* (m,b))) = x +* (m,v)
proof end;

theorem Th26: :: MIDSP_3:26
for n being 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 & (a,v) . W = b holds
(a,(x +* (m,v))) . W = p +* (m,b)
proof end;

theorem :: MIDSP_3:27
for n being 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 )
proof end;

theorem Th28: :: MIDSP_3:28
for n being 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) )
proof end;

theorem Th29: :: MIDSP_3:29
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n st RAS has_property_of_zero_in m & RAS is_additive_in m holds
RAS is_semi_additive_in m
proof end;

Lm6: for n being 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)))))) )

proof end;

Lm7: for n being 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

proof end;

theorem :: MIDSP_3:30
for n being 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))) )
proof end;

theorem Th31: :: MIDSP_3:31
for n being 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 & m <= n holds
W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m))
proof end;

theorem Th32: :: MIDSP_3:32
for n being 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 & m <= n holds
(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))
proof end;

theorem :: MIDSP_3:33
for n being 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 )
proof end;