:: Reper Algebras
:: by Micha{\l} Muzalewski
::
:: Received May 28, 1992
:: Copyright (c) 1992-2021 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 c₂ is strict ;
struct ReperAlgebraStr over n -> MidStr ;
aggr ReperAlgebraStr(# carrier, MIDPOINT, reper #) -> ReperAlgebraStr over n;
sel reper c₂ -> Function of (n -tuples_on the carrier of c₂), the carrier of c₂;

end;

registration

let n be 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 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 b₁ being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b₁ @ 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 b₁ being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b₁ @ 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 b₁ being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b₁ @ 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 b₁ being Element of the carrier of ReperAlgebraStr(# the carrier of M, the MIDPOINT of M,R #) st b₁ @ 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 b₁ being ReperAlgebraStr over n holds b₁ is empty

proof end;

end;

registration

let n be Nat;

cluster non empty MidSp-like for ReperAlgebraStr over n + 2;

existence
ex b₁ being non empty ReperAlgebraStr over n + 2 st b₁ 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 Lm1, Lm2;

definition

let n be Nat;

mode Nat of n -> Nat means :Def2: :: MIDSP_3:def 2
( 1 <= it & it <= n + 1 );

existence
ex b₁ being Nat st
( 1 <= b₁ & b₁ <= n + 1 )

proof end;

end;

:: deftheorem Def2 defines Nat MIDSP_3:def 2 :
for n, b₂ being Nat holds
( b₂ is Nat of n iff ( 1 <= b₂ & b₂ <= 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 Lm1, Lm2;

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{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

ex z being FinSequence of F₂() st
( len z = F₁() + 1 & ( for j being Nat of F₁() holds z . j = F₃(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 b₁ being Tuple of (n + 1),RAS st
for m being Nat of n holds b₁ . m = (a,(x . m)) . W

proof end;

uniqueness
for b₁, b₂ being Tuple of (n + 1),RAS st ( for m being Nat of n holds b₁ . m = (a,(x . m)) . W ) & ( for m being Nat of n holds b₂ . m = (a,(x . m)) . W ) holds
b₁ = b₂

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 b₆ being Tuple of (n + 1),RAS holds
( b₆ = (a,x) . W iff for m being Nat of n holds b₆ . 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 b₁ being Tuple of (n + 1),W st
for m being Nat of n holds b₁ . m = W . (a,(p . m))

proof end;

uniqueness
for b₁, b₂ being Tuple of (n + 1),W st ( for m being Nat of n holds b₁ . m = W . (a,(p . m)) ) & ( for m being Nat of n holds b₂ . m = W . (a,(p . m)) ) holds
b₁ = b₂

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 b₆ being Tuple of (n + 1),W holds
( b₆ = W . (a,p) iff for m being Nat of n holds b₆ . 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 b₁ being non empty MidSp-like ReperAlgebraStr over n + 2 st b₁ is being_invariance

proof end;

end;

:: deftheorem Def11 defines ReperAlgebra MIDSP_3:def 11 :
for n being Nat
for b₂ being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( b₂ is ReperAlgebra of n iff b₂ 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 Def11, Th19;

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 b₁ being Vector of W st
for a being Point of RAS holds b₁ = Phi (a,x)

proof end;

uniqueness
for b₁, b₂ being Vector of W st ( for a being Point of RAS holds b₁ = Phi (a,x) ) & ( for a being Point of RAS holds b₂ = Phi (a,x) ) holds
b₁ = b₂

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 b₅ being Vector of W holds
( b₅ = Phi x iff for a being Point of RAS holds b₅ = 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;