:: MIDSP_3 semantic presentation

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 & len r = k & p = (q ^ <*c*>) ^ r )
proof
let j, k be Element of NAT ; ::_thesis: 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 )
let D be non empty set ; ::_thesis: 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 )
let p be FinSequence of D; ::_thesis: ( len p = (j + 1) + k implies ex q, r being FinSequence of D ex c being Element of D st
( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) )
assume  len p = (j + 1) + k ; ::_thesis: ex q, r being FinSequence of D ex c being Element of D st
( len q = j & len r = k & p = (q ^ <*c*>) ^ r )
then consider q9, r being FinSequence of D such that
A1: len q9 = j + 1 and
A2: ( len r = k & p = q9 ^ r ) by FINSEQ_2:23;
consider q being FinSequence of D, c being Element of D such that
A3: q9 = q ^ <*c*> by A1, FINSEQ_2:19;
take  q ; ::_thesis: ex r being FinSequence of D ex c being Element of D st
( len q = j & len r = k & p = (q ^ <*c*>) ^ r )
take  r ; ::_thesis: ex c being Element of D st
( len q = j & len r = k & p = (q ^ <*c*>) ^ r )
take  c ; ::_thesis: ( len q = j & len r = k & p = (q ^ <*c*>) ^ r )
 len q9 = (len q) + 1 by A3, FINSEQ_2:16;
hence  ( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) by A1, A2, A3; ::_thesis: verum
end;

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 & i = j + 1 )
proof
let i, n be Element of NAT ; ::_thesis: ( i in Seg n implies ex j, k being Element of NAT st
( n = (j + 1) + k & i = j + 1 ) )
assume A1: i in Seg n ; ::_thesis: ex j, k being Element of NAT st
( n = (j + 1) + k & i = j + 1 )
then  1 <= i by FINSEQ_1:1;
then consider j being Nat such that
A2: i = 1 + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
 i <= n by A1, FINSEQ_1:1;
then consider k being Nat such that
A3: n = (j + 1) + k by A2, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take  j ; ::_thesis: ex k being Element of NAT st
( n = (j + 1) + k & i = j + 1 )
take  k ; ::_thesis: ( n = (j + 1) + k & i = j + 1 )
thus  ( n = (j + 1) + k & i = j + 1 ) by A2, A3; ::_thesis: verum
end;

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 & i = (len q) + 1 holds
( ( for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
proof
let i be Element of NAT ; ::_thesis: 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 Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
let D be non empty set ; ::_thesis: 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 Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
let c be Element of D; ::_thesis: for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds
( ( for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
let p, q, r be FinSequence of D; ::_thesis: ( p = (q ^ <*c*>) ^ r & i = (len q) + 1 implies ( ( for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) ) )
set q9 = q ^ <*c*>;
assume that
A1: p = (q ^ <*c*>) ^ r and
A2: i = (len q) + 1 ; ::_thesis: ( ( for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
A3: p = q ^ (<*c*> ^ r) by A1, FINSEQ_1:32;
thus  for l being Element of NAT st 1 <= l & l <= len q holds
p . l = q . l ::_thesis: ( p . i = c & ( for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
proof
let l be Element of NAT ; ::_thesis: ( 1 <= l & l <= len q implies p . l = q . l )
assume  ( 1 <= l & l <= len q ) ; ::_thesis: p . l = q . l
then  l in dom q by FINSEQ_3:25;
hence  p . l = q . l by A3, FINSEQ_1:def_7; ::_thesis: verum
end;
A4: len (q ^ <*c*>) = i by A2, FINSEQ_2:16;
 i in Seg i by A2, FINSEQ_1:3;
then  i in dom (q ^ <*c*>) by A4, FINSEQ_1:def_3;
hence p . i = (q ^ <*c*>) . i by A1, FINSEQ_1:def_7
.= c by A2, FINSEQ_1:42 ;
::_thesis: for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i)
 len p = (len (q ^ <*c*>)) + (len r) by A1, FINSEQ_1:22;
hence  for l being Element of NAT st i + 1 <= l & l <= len p holds
p . l = r . (l - i) by A1, A4, FINSEQ_1:23; ::_thesis: verum
end;

theorem Th4: :: MIDSP_3:4
for l, j being Element of NAT holds
( l <= j or l = j + 1 or j + 2 <= l )
proof
let l, j be Element of NAT ; ::_thesis: ( l <= j or l = j + 1 or j + 2 <= l )
A1: (j + 1) + 1 = j + 2 ;
 ( l < j + 1 or l = j + 1 or j + 1 < l ) by XXREAL_0:1;
hence  ( l <= j or l = j + 1 or j + 2 <= l ) by A1, NAT_1:13; ::_thesis: verum
end;

theorem :: MIDSP_3:5
for l, n, i, j being Element of NAT st l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) holds
( i + 1 <= l & l <= n )
proof
let l, n, i, j be Element of NAT ; ::_thesis: ( l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) implies ( i + 1 <= l & l <= n ) )
assume that
A1: l in (Seg n) \ {i} and
A2: i = j + 1 ; ::_thesis: ( ( 1 <= l & l <= j ) or ( i + 1 <= l & l <= n ) )
A3: i + 1 = j + 2 by A2;
 ( l in Seg n & l <> i ) by A1, ZFMISC_1:56;
hence  ( ( 1 <= l & l <= j ) or ( i + 1 <= l & l <= n ) ) by A2, A3, Th4, FINSEQ_1:1; ::_thesis: verum
end;

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
proof
 dom (p +* (i,d)) = dom p by FUNCT_7:30;
then  len (p +* (i,d)) = len p by FINSEQ_3:29
.= n by CARD_1:def_7 ;
hence  p +* (i,d) is Element of n -tuples_on D by FINSEQ_2:92; ::_thesis: verum
end;
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
proof
let n, i be Element of NAT ; ::_thesis: 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
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: for p being Element of n -tuples_on D st i in Seg n holds
(p +* (i,d)) . i = d
let p be Element of n -tuples_on D; ::_thesis: ( i in Seg n implies (p +* (i,d)) . i = d )
 Seg n = dom p by FINSEQ_2:124;
hence  ( i in Seg n implies (p +* (i,d)) . i = d ) by FUNCT_7:31; ::_thesis: verum
end;

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
proof
let n, i be Element of NAT ; ::_thesis: 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
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let p be Element of n -tuples_on D; ::_thesis: for l being Element of NAT st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
let l be Element of NAT ; ::_thesis: ( l in (dom p) \ {i} implies (p +* (i,d)) . l = p . l )
assume  l in (dom p) \ {i} ; ::_thesis: (p +* (i,d)) . l = p . l
then  not l in {i} by XBOOLE_0:def_5;
then  l <> i by TARSKI:def_1;
hence  (p +* (i,d)) . l = p . l by FUNCT_7:32; ::_thesis: verum
end;

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 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 Element of NAT ;
cluster non empty for ReperAlgebraStr over n;
existence
 not for b1 being ReperAlgebraStr over n holds b1 is empty
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
set r = the Function of (n -tuples_on the non empty set ), the non empty set ;
take  ReperAlgebraStr(# the non empty set , the BinOp of the non empty set , the Function of (n -tuples_on the non empty set ), the non empty set #) ; ::_thesis: not ReperAlgebraStr(# the non empty set , the BinOp of the non empty set , the Function of (n -tuples_on the non empty set ), the non empty set #) is empty
thus  not ReperAlgebraStr(# the non empty set , the BinOp of the non empty set , the Function of (n -tuples_on the non empty set ), the non empty set #) is empty ; ::_thesis: verum
end;
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
proof
set M = the MidSp;
set R = the Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp;
take  ReperAlgebraStr(# the carrier of the MidSp, the MIDPOINT of the MidSp, the Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp #) ; ::_thesis: ReperAlgebraStr(# the carrier of the MidSp, the MIDPOINT of the MidSp, the Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp #) is MidSp-like
thus  ReperAlgebraStr(# the carrier of the MidSp, the MIDPOINT of the MidSp, the Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp #) is MidSp-like by Lm3; ::_thesis: verum
end;
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
proof
reconsider p = p as Tuple of i, the carrier of RAS ;
reconsider q = q as Tuple of j, the carrier of RAS ;
 p ^ q is Tuple of i + j, the carrier of RAS by FINSEQ_2:107;
hence  p ^ q is Tuple of (i + j),RAS by FINSEQ_2:131; ::_thesis: verum
end;
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
proof
reconsider p9 = <*a*> ^ p as Tuple of (n + 2),RAS ;
 the reper of RAS . p9 is Point of RAS ;
hence  the reper of RAS . (<*a*> ^ p) is Point of RAS ; ::_thesis: verum
end;
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 & ( 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 & it <= n + 1 );
existence
 ex b1 being Element of NAT st
( 1 <= b1 & b1 <= n + 1 )
proof
take  1 ; ::_thesis: ( 1 <= 1 & 1 <= n + 1 )
 0 <= n by NAT_1:2;
then  0 + 1 <= n + 1 by XREAL_1:7;
hence  ( 1 <= 1 & 1 <= n + 1 ) ; ::_thesis: verum
end;
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 & 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) )
proof
let i, n be Element of NAT ; ::_thesis: ( i is Nat of n iff i in Seg (n + 1) )
 ( i is Nat of n iff ( 1 <= i & i <= n + 1 ) ) by Def2;
hence  ( i is Nat of n iff i in Seg (n + 1) ) by FINSEQ_1:1; ::_thesis: verum
end;

theorem Th8: :: MIDSP_3:8
for i, n being Element of NAT st i <= n holds
i + 1 is Nat of n
proof
let i, n be Element of NAT ; ::_thesis: ( i <= n implies i + 1 is Nat of n )
assume  i <= n ; ::_thesis: i + 1 is Nat of n
then A1: i + 1 <= n + 1 by XREAL_1:7;
 1 <= i + 1 by NAT_1:11;
hence  i + 1 is Nat of n by A1, Def2; ::_thesis: verum
end;

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
proof
let n be Element of NAT ; ::_thesis: 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
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds
p = q
let p, q be Tuple of (n + 1),RAS; ::_thesis: ( ( for m being Nat of n holds p . m = q . m ) implies p = q )
assume A1: for m being Nat of n holds p . m = q . m ; ::_thesis: p = q
 for j being Nat st j in Seg (n + 1) holds
p . j = q . j
proof
let j be Nat; ::_thesis: ( j in Seg (n + 1) implies p . j = q . j )
assume  j in Seg (n + 1) ; ::_thesis: p . j = q . j
then reconsider j = j as Nat of n by Th7;
 p . j = q . j by A1;
hence  p . j = q . j ; ::_thesis: verum
end;
hence  p = q by FINSEQ_2:119; ::_thesis: verum
end;

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
proof
let n, i be Element of NAT ; ::_thesis: 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
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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
let d be Point of RAS; ::_thesis: for p being Tuple of (n + 1),RAS
for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
let p be Tuple of (n + 1),RAS; ::_thesis: for l being Nat of n st l = i holds
(p +* (i,d)) . l = d
let l be Nat of n; ::_thesis: ( l = i implies (p +* (i,d)) . l = d )
assume A1: l = i ; ::_thesis: (p +* (i,d)) . l = d
 l in Seg (n + 1) by Th7;
hence  (p +* (i,d)) . l = d by A1, Lm1; ::_thesis: verum
end;

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
proof
reconsider S = Seg (n + 1) as non empty set by FINSEQ_1:4;
 ( m in S & len p = n + 1 ) by Th7, CARD_1:def_7;
then  m in dom p by FINSEQ_1:def_3;
then  ( rng p c= D & p . m in rng p ) by FINSEQ_1:def_4, FUNCT_1:def_3;
hence  p . m is Element of D ; ::_thesis: verum
end;
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
proof
thus  p +* (i,a) is Tuple of (n + 1),RAS ; ::_thesis: verum
end;
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))
proof
let n be Element of NAT ; ::_thesis: 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))
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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))
let m be Nat of n; ::_thesis: ( RAS is_semi_additive_in m implies 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)) )
assume A1: RAS is_semi_additive_in m ; ::_thesis: 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))
let a, d be Point of RAS; ::_thesis: for p, q being Tuple of (n + 1),RAS st q = p +* (m,d) holds
*' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))
let p, q be Tuple of (n + 1),RAS; ::_thesis: ( q = p +* (m,d) implies *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) )
set qq = q +* (m,(a @ d));
assume A2: q = p +* (m,d) ; ::_thesis: *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q))
A3: q +* (m,(a @ d)) = p +* (m,(a @ d))
proof
set pp = p +* (m,(a @ d));
 for k being Nat of n holds (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
proof
let k be Nat of n; ::_thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
now__::_thesis:_(q_+*_(m,(a_@_d)))_._k_=_(p_+*_(m,(a_@_d)))_._k
percases ( k = m or k <> m ) ;
supposeA4: k = m ; ::_thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
 (p +* (m,(a @ d))) . m = a @ d by Th10;
hence  (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k by A4, Th10; ::_thesis: verum
end;
supposeA5: k <> m ; ::_thesis: (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k
hence (q +* (m,(a @ d))) . k = q . k by FUNCT_7:32
.= p . k by A2, A5, FUNCT_7:32
.= (p +* (m,(a @ d))) . k by A5, FUNCT_7:32 ;
::_thesis: verum
end;
end;
end;
hence  (q +* (m,(a @ d))) . k = (p +* (m,(a @ d))) . k ; ::_thesis: verum
end;
hence  q +* (m,(a @ d)) = p +* (m,(a @ d)) by Th9; ::_thesis: verum
end;
 q . m = d by A2, Th10;
hence  *' (a,(p +* (m,(a @ d)))) = a @ (*' (a,q)) by A1, A3, Def5; ::_thesis: verum
end;

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 & ( 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 ) & ( for l, i being Nat of n st l <> i holds
(x +* (i,v)) . l = x . l ) )
proof
let n, i be Element of NAT ; ::_thesis: 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 ) )
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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 ) )
let W be ATLAS of RAS; ::_thesis: 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 ) )
let v be Vector of W; ::_thesis: 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 ) )
let x be Tuple of (n + 1),W; ::_thesis: ( ( 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 ) )
thus  for l being Nat of n st l = i holds
(x +* (i,v)) . l = v ::_thesis: for l, i being Nat of n st l <> i holds
(x +* (i,v)) . l = x . l
proof
let l be Nat of n; ::_thesis: ( l = i implies (x +* (i,v)) . l = v )
assume A1: l = i ; ::_thesis: (x +* (i,v)) . l = v
 l in Seg (n + 1) by Th7;
hence  (x +* (i,v)) . l = v by A1, Lm1; ::_thesis: verum
end;
thus  for l, i being Nat of n st l <> i holds
(x +* (i,v)) . l = x . l by FUNCT_7:32; ::_thesis: verum
end;

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
proof
let n be Element of NAT ; ::_thesis: 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
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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
let W be ATLAS of RAS; ::_thesis: for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds
x = y
let x, y be Tuple of (n + 1),W; ::_thesis: ( ( for m being Nat of n holds x . m = y . m ) implies x = y )
assume A1: for m being Nat of n holds x . m = y . m ; ::_thesis: x = y
 for j being Nat st j in Seg (n + 1) holds
x . j = y . j
proof
let j be Nat; ::_thesis: ( j in Seg (n + 1) implies x . j = y . j )
assume  j in Seg (n + 1) ; ::_thesis: x . j = y . j
then reconsider j = j as Nat of n by Th7;
 x . j = y . j by A1;
hence  x . j = y . j ; ::_thesis: verum
end;
hence  x = y by FINSEQ_2:119; ::_thesis: verum
end;

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 & ( for j being Nat of F1() holds z . j = F3(j) ) )
proof
reconsider S = Seg (F1() + 1) as non empty set by FINSEQ_1:4;
consider z being FinSequence of F2() such that
A1: len z = F1() + 1 and
A2: for j being Nat st j in dom z holds
z . j = F3(j) from FINSEQ_2:sch_1();
take  z ; ::_thesis: ( len z = F1() + 1 & ( for j being Nat of F1() holds z . j = F3(j) ) )
A3: dom z = Seg (F1() + 1) by A1, FINSEQ_1:def_3;
 for j being Nat of F1() holds z . j = F3(j)
proof
let j be Nat of F1(); ::_thesis: z . j = F3(j)
 j in S by Th7;
hence  z . j = F3(j) by A2, A3; ::_thesis: verum
end;
hence  ( len z = F1() + 1 & ( for j being Nat of F1() holds z . j = F3(j) ) ) by A1; ::_thesis: verum
end;

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
proof
deffunc H1( Nat of n) ->  Element of the carrier of RAS = (a,(x . $1)) . W;
consider z being FinSequence of the carrier of RAS such that
A1: len z = n + 1 and
A2: for m being Nat of n holds z . m = H1(m) from MIDSP_3:sch_1();
reconsider z = z as Tuple of (n + 1),RAS by A1, FINSEQ_2:92;
take  z ; ::_thesis: for m being Nat of n holds z . m = (a,(x . m)) . W
thus  for m being Nat of n holds z . m = (a,(x . m)) . W by A2; ::_thesis: verum
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
let p, q be Tuple of (n + 1),RAS; ::_thesis: ( ( for m being Nat of n holds p . m = (a,(x . m)) . W ) & ( for m being Nat of n holds q . m = (a,(x . m)) . W ) implies p = q )
assume that
A3: for m being Nat of n holds p . m = (a,(x . m)) . W and
A4: for m being Nat of n holds q . m = (a,(x . m)) . W ; ::_thesis: p = q
 for m being Nat of n holds p . m = q . m
proof
let m be Nat of n; ::_thesis: p . m = q . m
 p . m = (a,(x . m)) . W by A3;
hence  p . m = q . m by A4; ::_thesis: verum
end;
hence  p = q by Th9; ::_thesis: verum
end;
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))
proof
deffunc H1( Nat of n) ->  Element of the carrier of the algebra of W = W . (a,(p . $1));
consider z being FinSequence of the carrier of the algebra of W such that
A1: len z = n + 1 and
A2: for m being Nat of n holds z . m = H1(m) from MIDSP_3:sch_1();
reconsider z = z as Tuple of (n + 1),W by A1, FINSEQ_2:92;
take  z ; ::_thesis: for m being Nat of n holds z . m = W . (a,(p . m))
thus  for m being Nat of n holds z . m = W . (a,(p . m)) by A2; ::_thesis: verum
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
let x, y be Tuple of (n + 1),W; ::_thesis: ( ( for m being Nat of n holds x . m = W . (a,(p . m)) ) & ( for m being Nat of n holds y . m = W . (a,(p . m)) ) implies x = y )
assume that
A3: for m being Nat of n holds x . m = W . (a,(p . m)) and
A4: for m being Nat of n holds y . m = W . (a,(p . m)) ; ::_thesis: x = y
 for m being Nat of n holds x . m = y . m
proof
let m be Nat of n; ::_thesis: x . m = y . m
 W . (a,(p . m)) = x . m by A3;
hence  x . m = y . m by A4; ::_thesis: verum
end;
hence  x = y by Th14; ::_thesis: verum
end;
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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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 )
let a be Point of RAS; ::_thesis: 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 )
let p be Tuple of (n + 1),RAS; ::_thesis: for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . (a,p) = x iff (a,x) . W = p )
let W be ATLAS of RAS; ::_thesis: for x being Tuple of (n + 1),W holds
( W . (a,p) = x iff (a,x) . W = p )
let x be Tuple of (n + 1),W; ::_thesis: ( W . (a,p) = x iff (a,x) . W = p )
thus  ( W . (a,p) = x implies (a,x) . W = p ) ::_thesis: ( (a,x) . W = p implies W . (a,p) = x )
proof
assume A1: W . (a,p) = x ; ::_thesis: (a,x) . W = p
now__::_thesis:_for_m_being_Nat_of_n_holds_(a,(x_._m))_._W_=_p_._m
let m be Nat of n; ::_thesis: (a,(x . m)) . W = p . m
 W . (a,(p . m)) = x . m by A1, Def9;
hence  (a,(x . m)) . W = p . m by MIDSP_2:33; ::_thesis: verum
end;
hence  (a,x) . W = p by Def8; ::_thesis: verum
end;
thus  ( (a,x) . W = p implies W . (a,p) = x ) ::_thesis: verum
proof
assume A2: (a,x) . W = p ; ::_thesis: W . (a,p) = x
now__::_thesis:_for_m_being_Nat_of_n_holds_W_._(a,(p_._m))_=_x_._m
let m be Nat of n; ::_thesis: W . (a,(p . m)) = x . m
 (a,(x . m)) . W = p . m by A2, Def8;
hence  W . (a,(p . m)) = x . m by MIDSP_2:33; ::_thesis: verum
end;
hence  W . (a,p) = x by Def9; ::_thesis: verum
end;
end;

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 & W . (a,b) = v holds
( *' (a,p) = b iff Phi (a,x) = v )
proof
let n be Element of NAT ; ::_thesis: 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 )
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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 )
let a, b be Point of RAS; ::_thesis: 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 )
let p be Tuple of (n + 1),RAS; ::_thesis: 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 )
let W be ATLAS of RAS; ::_thesis: 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 )
let v be Vector of W; ::_thesis: 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 )
let x be Tuple of (n + 1),W; ::_thesis: ( W . (a,p) = x & W . (a,b) = v implies ( *' (a,p) = b iff Phi (a,x) = v ) )
assume that
A1: W . (a,p) = x and
A2: W . (a,b) = v ; ::_thesis: ( *' (a,p) = b iff Phi (a,x) = v )
 Phi (a,x) = W . (a,(*' (a,p))) by A1, Th15;
hence  ( *' (a,p) = b iff Phi (a,x) = v ) by A2, MIDSP_2:32; ::_thesis: verum
end;

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) )
proof
let n be Element of NAT ; ::_thesis: 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) )
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; ::_thesis: 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) )
let W be ATLAS of RAS; ::_thesis: ( 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) )
A1: ( ( for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ) implies RAS is being_invariance )
proof
assume A2: for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ; ::_thesis: RAS is being_invariance
let a be Point of RAS; :: according to MIDSP_3:def_3 ::_thesis: for 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))
let b be Point of RAS; ::_thesis: 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))
let p, q be Tuple of (n + 1),RAS; ::_thesis: ( ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) implies a @ (*' (b,q)) = b @ (*' (a,p)) )
A3: W . (a,(*' (a,((a,(W . (a,p))) . W)))) = Phi (a,(W . (a,p)))
.= Phi (b,(W . (a,p))) by A2
.= W . (b,(*' (b,((b,(W . (a,p))) . W)))) ;
assume A4: for m being Nat of n holds a @ (q . m) = b @ (p . m) ; ::_thesis: a @ (*' (b,q)) = b @ (*' (a,p))
A5: now__::_thesis:_for_m_being_Nat_of_n_holds_(W_._(a,p))_._m_=_(W_._(b,q))_._m
let m be Nat of n; ::_thesis: (W . (a,p)) . m = (W . (b,q)) . m
 a @ (q . m) = b @ (p . m) by A4;
then A6: W . (a,(p . m)) = W . (b,(q . m)) by MIDSP_2:33;
thus (W . (a,p)) . m = W . (a,(p . m)) by Def9
.= (W . (b,q)) . m by A6, Def9 ; ::_thesis: verum
end;
W . (a,(*' (a,p))) = W . (a,(*' (a,((a,(W . (a,p))) . W)))) by Th15
.= W . (b,(*' (b,((b,(W . (b,q))) . W)))) by A5, A3, Th14
.= W . (b,(*' (b,q))) by Th15 ;
hence  a @ (*' (b,q)) = b @ (*' (a,p)) by MIDSP_2:33; ::_thesis: verum
end;
now__::_thesis:_(_RAS_is_being_invariance_implies_for_a,_b_being_Point_of_RAS
for_x_being_Tuple_of_(n_+_1),W_holds_Phi_(a,x)_=_Phi_(b,x)_)
assume A7: RAS is being_invariance ; ::_thesis: for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let a, b be Point of RAS; ::_thesis: for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let x be Tuple of (n + 1),W; ::_thesis: Phi (a,x) = Phi (b,x)
set p = (a,x) . W;
set q = (b,x) . W;
A8: W . (a,((a,x) . W)) = x by Th15
.= W . (b,((b,x) . W)) by Th15 ;
now__::_thesis:_for_m_being_Nat_of_n_holds_a_@_(((b,x)_._W)_._m)_=_b_@_(((a,x)_._W)_._m)
let m be Nat of n; ::_thesis: a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m)
W . (a,(((a,x) . W) . m)) = (W . (a,((a,x) . W))) . m by Def9
.= W . (b,(((b,x) . W) . m)) by A8, Def9 ;
hence  a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m) by MIDSP_2:33; ::_thesis: verum
end;
then  a @ (*' (b,((b,x) . W))) = b @ (*' (a,((a,x) . W))) by A7, Def3;
hence  Phi (a,x) = Phi (b,x) by MIDSP_2:33; ::_thesis: verum
end;
hence  ( 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) ) by A1; ::_thesis: verum
end;

theorem Th20: :: MIDSP_3:20
for n being Element of NAT holds 1 in Seg (n + 1)
proof
let n be Element of NAT ; ::_thesis: 1 in Seg (n + 1)
 0 <= n by NAT_1:2;
then  0 + 1 <= n + 1 by XREAL_1:7;
hence  1 in Seg (n + 1) by FINSEQ_1:1; ::_thesis: verum
end;

theorem Th21: :: MIDSP_3:21
for n being Element of NAT holds 1 is Nat of n
proof
let n be Element of NAT ; ::_thesis: 1 is Nat of n
 1 in Seg (n + 1) by Th20;
hence  1 is Nat of n by Th7; ::_thesis: verum
end;

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
proof
reconsider one1 = 1 as Nat of n + 1 by Th21;
set M = the MidSp;
set D = the carrier of the MidSp;
set k = (n + 1) + 1;
set C = ((n + 1) + 1) -tuples_on the carrier of the MidSp;
deffunc H1( Element of ((n + 1) + 1) -tuples_on the carrier of the MidSp) ->  Element of the carrier of the MidSp = $1 . one1;
consider R being Function of (((n + 1) + 1) -tuples_on the carrier of the MidSp), the carrier of the MidSp such that
A1: for p being Element of ((n + 1) + 1) -tuples_on the carrier of the MidSp holds R . p = H1(p) from FUNCT_2:sch_4();
reconsider R = R as Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp ;
reconsider RA = ReperAlgebraStr(# the carrier of the MidSp, the MIDPOINT of the MidSp,R #) as non empty MidSp-like ReperAlgebraStr over n + 2 by Lm3;
take  RA ; ::_thesis: RA is being_invariance
 for a, b being Point of RA
for p, q being Tuple of (n + 1),RA st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p))
proof
let a, b be Point of RA; ::_thesis: for p, q being Tuple of (n + 1),RA st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p))
let p, q be Tuple of (n + 1),RA; ::_thesis: ( ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) implies a @ (*' (b,q)) = b @ (*' (a,p)) )
assume  for m being Nat of n holds a @ (q . m) = b @ (p . m) ; ::_thesis: a @ (*' (b,q)) = b @ (*' (a,p))
A2: *' (a,p) = (<*a*> ^ p) . one1 by A1
.= a by FINSEQ_1:41 ;
*' (b,q) = (<*b*> ^ q) . one1 by A1
.= b by FINSEQ_1:41 ;
hence  a @ (*' (b,q)) = b @ (*' (a,p)) by A2; ::_thesis: verum
end;
hence  RA is being_invariance by Def3; ::_thesis: verum
end;
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)
proof
let n be Element of NAT ; ::_thesis: 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)
let RAS be ReperAlgebra of n; ::_thesis: 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)
let a, b be Point of RAS; ::_thesis: for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let W be ATLAS of RAS; ::_thesis: for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let x be Tuple of (n + 1),W; ::_thesis: Phi (a,x) = Phi (b,x)
 RAS is being_invariance by Def11;
hence  Phi (a,x) = Phi (b,x) by Th19; ::_thesis: verum
end;

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)
proof
set a = the Point of RAS;
take  Phi ( the Point of RAS,x) ; ::_thesis: for a being Point of RAS holds Phi ( the Point of RAS,x) = Phi (a,x)
thus  for a being Point of RAS holds Phi ( the Point of RAS,x) = Phi (a,x) by Th22; ::_thesis: verum
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
set a = the Point of RAS;
let y, z be Vector of W; ::_thesis: ( ( for a being Point of RAS holds y = Phi (a,x) ) & ( for a being Point of RAS holds z = Phi (a,x) ) implies y = z )
assume that
A1: for a being Point of RAS holds y = Phi (a,x) and
A2: for a being Point of RAS holds z = Phi (a,x) ; ::_thesis: y = z
 y = Phi ( the Point of RAS,x) by A1;
hence  y = z by A2; ::_thesis: verum
end;
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)))
proof
let n be Element of NAT ; ::_thesis: 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)))
let RAS be ReperAlgebra of n; ::_thesis: 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)))
let a be Point of RAS; ::_thesis: 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)))
let p be Tuple of (n + 1),RAS; ::_thesis: 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)))
let W be ATLAS of RAS; ::_thesis: for x being Tuple of (n + 1),W st W . (a,p) = x holds
Phi x = W . (a,(*' (a,p)))
let x be Tuple of (n + 1),W; ::_thesis: ( W . (a,p) = x implies Phi x = W . (a,(*' (a,p))) )
assume A1: W . (a,p) = x ; ::_thesis: Phi x = W . (a,(*' (a,p)))
thus  Phi x = Phi (a,x) by Def12
.= W . (a,(*' (a,p))) by A1, Th15 ; ::_thesis: verum
end;

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)))
proof
let n be Element of NAT ; ::_thesis: 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)))
let RAS be ReperAlgebra of n; ::_thesis: 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)))
let a be Point of RAS; ::_thesis: 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)))
let p be Tuple of (n + 1),RAS; ::_thesis: 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)))
let W be ATLAS of RAS; ::_thesis: for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
let x be Tuple of (n + 1),W; ::_thesis: ( (a,x) . W = p implies Phi x = W . (a,(*' (a,p))) )
assume  (a,x) . W = p ; ::_thesis: Phi x = W . (a,(*' (a,p)))
then  W . (a,p) = x by Th15;
hence  Phi x = W . (a,(*' (a,p))) by Lm4; ::_thesis: verum
end;

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 & W . (a,b) = v & Phi x = v holds
*' (a,p) = b
proof
let n be Element of NAT ; ::_thesis: 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
let RAS be ReperAlgebra of n; ::_thesis: 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
let a, b be Point of RAS; ::_thesis: 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
let p be Tuple of (n + 1),RAS; ::_thesis: 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
let W be ATLAS of RAS; ::_thesis: 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
let v be Vector of W; ::_thesis: for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds
*' (a,p) = b
let x be Tuple of (n + 1),W; ::_thesis: ( W . (a,p) = x & W . (a,b) = v & Phi x = v implies *' (a,p) = b )
assume A1: ( W . (a,p) = x & W . (a,b) = v & Phi x = v ) ; ::_thesis: *' (a,p) = b
 Phi x = Phi (a,x) by Def12;
hence  *' (a,p) = b by A1, Th18; ::_thesis: verum
end;

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 & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
proof
let n be Element of NAT ; ::_thesis: 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
let RAS be ReperAlgebra of n; ::_thesis: 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
let a, b be Point of RAS; ::_thesis: 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
let p be Tuple of (n + 1),RAS; ::_thesis: 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
let W be ATLAS of RAS; ::_thesis: 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
let v be Vector of W; ::_thesis: for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let x be Tuple of (n + 1),W; ::_thesis: ( (a,x) . W = p & (a,v) . W = b & *' (a,p) = b implies Phi x = v )
assume  ( (a,x) . W = p & (a,v) . W = b & *' (a,p) = b ) ; ::_thesis: Phi x = v
then  Phi (a,x) = v by MIDSP_2:33;
hence  Phi x = v by Def12; ::_thesis: verum
end;

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 & W . (a,b) = v holds
W . (a,(p +* (m,b))) = x +* (m,v)
proof
let n be Element of NAT ; ::_thesis: 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)
let m be Nat of n; ::_thesis: 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)
let RAS be ReperAlgebra of n; ::_thesis: 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)
let a, b be Point of RAS; ::_thesis: 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)
let p be Tuple of (n + 1),RAS; ::_thesis: 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)
let W be ATLAS of RAS; ::_thesis: 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)
let v be Vector of W; ::_thesis: 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)
let x be Tuple of (n + 1),W; ::_thesis: ( W . (a,p) = x & W . (a,b) = v implies W . (a,(p +* (m,b))) = x +* (m,v) )
assume that
A1: W . (a,p) = x and
A2: W . (a,b) = v ; ::_thesis: W . (a,(p +* (m,b))) = x +* (m,v)
set q = p +* (m,b);
set y = W . (a,(p +* (m,b)));
set z = x +* (m,v);
 for k being Nat of n holds (W . (a,(p +* (m,b)))) . k = (x +* (m,v)) . k
proof
let k be Nat of n; ::_thesis: (W . (a,(p +* (m,b)))) . k = (x +* (m,v)) . k
now__::_thesis:_(W_._(a,(p_+*_(m,b))))_._k_=_(x_+*_(m,v))_._k
percases ( k = m or k <> m ) ;
supposeA3: k = m ; ::_thesis: (W . (a,(p +* (m,b)))) . k = (x +* (m,v)) . k
thus (W . (a,(p +* (m,b)))) . k = W . (a,((p +* (m,b)) . k)) by Def9
.= W . (a,b) by A3, Th10
.= (x +* (m,v)) . k by A2, A3, Th13 ; ::_thesis: verum
end;
supposeA4: k <> m ; ::_thesis: (W . (a,(p +* (m,b)))) . k = (x +* (m,v)) . k
thus (W . (a,(p +* (m,b)))) . k = W . (a,((p +* (m,b)) . k)) by Def9
.= W . (a,(p . k)) by A4, FUNCT_7:32
.= x . k by A1, Def9
.= (x +* (m,v)) . k by A4, FUNCT_7:32 ; ::_thesis: verum
end;
end;
end;
hence  (W . (a,(p +* (m,b)))) . k = (x +* (m,v)) . k ; ::_thesis: verum
end;
hence  W . (a,(p +* (m,b))) = x +* (m,v) by Th14; ::_thesis: verum
end;

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 & (a,v) . W = b holds
(a,(x +* (m,v))) . W = p +* (m,b)
proof
let n be Element of NAT ; ::_thesis: 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)
let m be Nat of n; ::_thesis: 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)
let RAS be ReperAlgebra of n; ::_thesis: 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)
let a, b be Point of RAS; ::_thesis: 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)
let p be Tuple of (n + 1),RAS; ::_thesis: 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)
let W be ATLAS of RAS; ::_thesis: 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)
let v be Vector of W; ::_thesis: 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)
let x be Tuple of (n + 1),W; ::_thesis: ( (a,x) . W = p & (a,v) . W = b implies (a,(x +* (m,v))) . W = p +* (m,b) )
assume  ( (a,x) . W = p & (a,v) . W = b ) ; ::_thesis: (a,(x +* (m,v))) . W = p +* (m,b)
then  ( W . (a,p) = x & W . (a,b) = v ) by Th15, MIDSP_2:33;
then  W . (a,(p +* (m,b))) = x +* (m,v) by Th25;
hence  (a,(x +* (m,v))) . W = p +* (m,b) by Th15; ::_thesis: verum
end;

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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let m be Nat of n; ::_thesis: 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 )
let RAS be ReperAlgebra of n; ::_thesis: 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 )
let W be ATLAS of RAS; ::_thesis: ( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W )
thus  ( RAS has_property_of_zero_in m implies for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ) ::_thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ) implies RAS has_property_of_zero_in m )
proof
set a = the Point of RAS;
assume A1: RAS has_property_of_zero_in m ; ::_thesis: for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W
set b = ( the Point of RAS,(0. W)) . W;
let x be Tuple of (n + 1),W; ::_thesis: Phi (x +* (m,(0. W))) = 0. W
set p9 = (( the Point of RAS,x) . W) +* (m, the Point of RAS);
A2: ( the Point of RAS,(0. W)) . W = the Point of RAS by MIDSP_2:34;
then A3: ( the Point of RAS,(x +* (m,(0. W)))) . W = (( the Point of RAS,x) . W) +* (m, the Point of RAS) by Th26;
 *' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m, the Point of RAS))) = ( the Point of RAS,(0. W)) . W by A1, A2, Def4;
hence  Phi (x +* (m,(0. W))) = 0. W by A3, Th24; ::_thesis: verum
end;
thus  ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ) implies RAS has_property_of_zero_in m ) ::_thesis: verum
proof
assume A4: for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ; ::_thesis: RAS has_property_of_zero_in m
 for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (m,a))) = a
proof
let a be Point of RAS; ::_thesis: for p being Tuple of (n + 1),RAS holds *' (a,(p +* (m,a))) = a
let p be Tuple of (n + 1),RAS; ::_thesis: *' (a,(p +* (m,a))) = a
set v = W . (a,a);
set x9 = (W . (a,p)) +* (m,(0. W));
 W . (a,a) = 0. W by MIDSP_2:33;
then  ( W . (a,(p +* (m,a))) = (W . (a,p)) +* (m,(0. W)) & Phi ((W . (a,p)) +* (m,(0. W))) = W . (a,a) ) by A4, Th25;
hence  *' (a,(p +* (m,a))) = a by Th23; ::_thesis: verum
end;
hence  RAS has_property_of_zero_in m by Def4; ::_thesis: verum
end;
end;

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) )
proof
let n be Element of NAT ; ::_thesis: 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) )
let m be Nat of n; ::_thesis: 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) )
let RAS be ReperAlgebra of n; ::_thesis: 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) )
let W be ATLAS of RAS; ::_thesis: ( 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) )
thus  ( RAS is_semi_additive_in m implies for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ) ::_thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ) implies RAS is_semi_additive_in m )
proof
set a = the Point of RAS;
assume A1: RAS is_semi_additive_in m ; ::_thesis: for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x)
let x be Tuple of (n + 1),W; ::_thesis: Phi (x +* (m,(Double (x . m)))) = Double (Phi x)
set x9 = x +* (m,(Double (x . m)));
set p = ( the Point of RAS,x) . W;
set p9 = ( the Point of RAS,(x +* (m,(Double (x . m))))) . W;
set q = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)));
 for i being Nat of n holds (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i
proof
let i be Nat of n; ::_thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i
now__::_thesis:_((_the_Point_of_RAS,x)_._W)_._i_=_(((_the_Point_of_RAS,(x_+*_(m,(Double_(x_._m)))))_._W)_+*_(m,(_the_Point_of_RAS_@_(((_the_Point_of_RAS,(x_+*_(m,(Double_(x_._m)))))_._W)_._m))))_._i
percases ( i = m or i <> m ) ;
supposeA2: i = m ; ::_thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i
 W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x by Th15;
then A3: W . ( the Point of RAS,((( the Point of RAS,x) . W) . m)) = x . m by Def9;
 W . ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)) = x +* (m,(Double (x . m))) by Th15;
then A4: W . ( the Point of RAS,((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)) = (x +* (m,(Double (x . m)))) . m by Def9;
 (x +* (m,(Double (x . m)))) . m = Double (x . m) by Th13;
then (( the Point of RAS,x) . W) . m = the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m) by A3, A4, MIDSP_2:31
.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . m by Th10 ;
hence  (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A2; ::_thesis: verum
end;
supposeA5: i <> m ; ::_thesis: (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i
thus (( the Point of RAS,x) . W) . i = ( the Point of RAS,(x . i)) . W by Def8
.= ( the Point of RAS,((x +* (m,(Double (x . m)))) . i)) . W by A5, FUNCT_7:32
.= (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . i by Def8
.= ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i by A5, FUNCT_7:32 ; ::_thesis: verum
end;
end;
end;
hence  (( the Point of RAS,x) . W) . i = ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m)))) . i ; ::_thesis: verum
end;
then  ( the Point of RAS,x) . W = (( the Point of RAS,(x +* (m,(Double (x . m))))) . W) +* (m,( the Point of RAS @ ((( the Point of RAS,(x +* (m,(Double (x . m))))) . W) . m))) by Th9;
then  *' ( the Point of RAS,(( the Point of RAS,x) . W)) = the Point of RAS @ (*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W))) by A1, Def5;
then A6: W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) = Double (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) by MIDSP_2:31;
 Phi (x +* (m,(Double (x . m)))) = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,(x +* (m,(Double (x . m))))) . W)))) by Lm5;
hence  Phi (x +* (m,(Double (x . m)))) = Double (Phi x) by A6, Lm5; ::_thesis: verum
end;
thus  ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ) implies RAS is_semi_additive_in m ) ::_thesis: verum
proof
assume A7: for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x) ; ::_thesis: RAS is_semi_additive_in m
let a be Point of RAS; :: according to MIDSP_3:def_5 ::_thesis: for pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pii holds
*' (a,(p +* (m,(a @ pii)))) = a @ (*' (a,p))
let p9m be Point of RAS; ::_thesis: for p being Tuple of (n + 1),RAS st p . m = p9m holds
*' (a,(p +* (m,(a @ p9m)))) = a @ (*' (a,p))
let p9 be Tuple of (n + 1),RAS; ::_thesis: ( p9 . m = p9m implies *' (a,(p9 +* (m,(a @ p9m)))) = a @ (*' (a,p9)) )
assume A8: p9 . m = p9m ; ::_thesis: *' (a,(p9 +* (m,(a @ p9m)))) = a @ (*' (a,p9))
set p = p9 +* (m,(a @ (p9 . m)));
set x = W . (a,(p9 +* (m,(a @ (p9 . m)))));
set x9 = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)));
 W . (a,p9) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))
proof
set y = W . (a,p9);
 for i being Nat of n holds ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i
proof
let i be Nat of n; ::_thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i
now__::_thesis:_((W_._(a,(p9_+*_(m,(a_@_(p9_._m))))))_+*_(m,(Double_((W_._(a,(p9_+*_(m,(a_@_(p9_._m))))))_._m))))_._i_=_(W_._(a,p9))_._i
percases ( i = m or i <> m ) ;
supposeA9: i = m ; ::_thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i
A10: ( W . (a,((p9 +* (m,(a @ (p9 . m)))) . m)) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m & (p9 +* (m,(a @ (p9 . m)))) . m = a @ (p9 . m) ) by Def9, Th10;
 ( ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . m = Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m) & W . (a,(p9 . m)) = (W . (a,p9)) . m ) by Def9, Th13;
hence  ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i by A9, A10, MIDSP_2:31; ::_thesis: verum
end;
supposeA11: i <> m ; ::_thesis: ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i
hence ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) . i by FUNCT_7:32
.= W . (a,((p9 +* (m,(a @ (p9 . m)))) . i)) by Def9
.= W . (a,(p9 . i)) by A11, FUNCT_7:32
.= (W . (a,p9)) . i by Def9 ;
::_thesis: verum
end;
end;
end;
hence  ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) . i = (W . (a,p9)) . i ; ::_thesis: verum
end;
hence  W . (a,p9) = (W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m))) by Th14; ::_thesis: verum
end;
then A12: Phi ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) +* (m,(Double ((W . (a,(p9 +* (m,(a @ (p9 . m)))))) . m)))) = W . (a,(*' (a,p9))) by Lm4;
 Phi (W . (a,(p9 +* (m,(a @ (p9 . m)))))) = W . (a,(*' (a,(p9 +* (m,(a @ (p9 . m))))))) by Lm4;
then  W . (a,(*' (a,p9))) = Double (W . (a,(*' (a,(p9 +* (m,(a @ (p9 . m)))))))) by A7, A12;
hence  *' (a,(p9 +* (m,(a @ p9m)))) = a @ (*' (a,p9)) by A8, MIDSP_2:31; ::_thesis: verum
end;
end;

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 & RAS is_additive_in m holds
RAS is_semi_additive_in m
proof
let n be Element of NAT ; ::_thesis: 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
let m be Nat of n; ::_thesis: 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
let RAS be ReperAlgebra of n; ::_thesis: ( RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS is_semi_additive_in m )
assume that
A1: RAS has_property_of_zero_in m and
A2: RAS is_additive_in m ; ::_thesis: RAS is_semi_additive_in m
let a be Point of RAS; :: according to MIDSP_3:def_5 ::_thesis: for pii being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pii holds
*' (a,(p +* (m,(a @ pii)))) = a @ (*' (a,p))
let pm be Point of RAS; ::_thesis: for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p))
let p be Tuple of (n + 1),RAS; ::_thesis: ( p . m = pm implies *' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p)) )
assume  p . m = pm ; ::_thesis: *' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p))
then  *' (a,(p +* (m,(a @ pm)))) = (*' (a,p)) @ (*' (a,(p +* (m,a)))) by A2, Def6
.= a @ (*' (a,p)) by A1, Def4 ;
hence  *' (a,(p +* (m,(a @ pm)))) = a @ (*' (a,p)) ; ::_thesis: verum
end;

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)))))) )
proof
let n be Element of NAT ; ::_thesis: 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)))))) )
let m be Nat of n; ::_thesis: 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)))))) )
let RAS be ReperAlgebra of n; ::_thesis: 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)))))) )
let W be ATLAS of RAS; ::_thesis: ( RAS is_semi_additive_in m implies 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)))))) ) )
assume A1: RAS is_semi_additive_in m ; ::_thesis: 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)))))) )
let a, p9m, p99m be Point of RAS; ::_thesis: 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)))))) )
let p be Tuple of (n + 1),RAS; ::_thesis: ( a @ p99m = (p . m) @ p9m implies ( *' (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)))))) ) )
assume  a @ p99m = (p . m) @ p9m ; ::_thesis: ( *' (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)))))) )
then  *' (a,(p +* (m,((p . m) @ p9m)))) = a @ (*' (a,(p +* (m,p99m)))) by A1, Th11;
hence  ( *' (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)))))) ) by MIDSP_2:30; ::_thesis: verum
end;

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
proof
let n be Element of NAT ; ::_thesis: 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
let m be Nat of n; ::_thesis: 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
let RAS be ReperAlgebra of n; ::_thesis: 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
let W be ATLAS of RAS; ::_thesis: ( ( 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))) ) implies RAS is_semi_additive_in m )
assume A1: 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))) ; ::_thesis: RAS is_semi_additive_in m
 for x being Tuple of (n + 1),W holds Phi (x +* (m,(Double (x . m)))) = Double (Phi x)
proof
let x be Tuple of (n + 1),W; ::_thesis: Phi (x +* (m,(Double (x . m)))) = Double (Phi x)
set v = x . m;
set y = x +* (m,(x . m));
 for k being Nat of n holds (x +* (m,(x . m))) . k = x . k
proof
let k be Nat of n; ::_thesis: (x +* (m,(x . m))) . k = x . k
now__::_thesis:_(x_+*_(m,(x_._m)))_._k_=_x_._k
percases ( k = m or k <> m ) ;
suppose k = m ; ::_thesis: (x +* (m,(x . m))) . k = x . k
hence  (x +* (m,(x . m))) . k = x . k by Th13; ::_thesis: verum
end;
suppose k <> m ; ::_thesis: (x +* (m,(x . m))) . k = x . k
hence  (x +* (m,(x . m))) . k = x . k by FUNCT_7:32; ::_thesis: verum
end;
end;
end;
hence  (x +* (m,(x . m))) . k = x . k ; ::_thesis: verum
end;
then A2: x +* (m,(x . m)) = x by Th14;
thus  Phi (x +* (m,(Double (x . m)))) = Phi (x +* (m,((x . m) + (x . m)))) by MIDSP_2:def_1
.= (Phi x) + (Phi (x +* (m,(x . m)))) by A1
.= Double (Phi x) by A2, MIDSP_2:def_1 ; ::_thesis: verum
end;
hence  RAS is_semi_additive_in m by Th28; ::_thesis: verum
end;

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))) )
proof
let n be Element of NAT ; ::_thesis: 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))) )
let m be Nat of n; ::_thesis: 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))) )
let RAS be ReperAlgebra of n; ::_thesis: 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))) )
let W be ATLAS of RAS; ::_thesis: ( RAS has_property_of_zero_in m implies ( 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))) ) )
assume A1: RAS has_property_of_zero_in m ; ::_thesis: ( 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))) )
thus  ( RAS is_additive_in m implies 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))) ) ::_thesis: ( ( 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))) ) implies RAS is_additive_in m )
proof
set a = the Point of RAS;
assume A2: RAS is_additive_in m ; ::_thesis: 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)))
let x be Tuple of (n + 1),W; ::_thesis: for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
let v be Vector of W; ::_thesis: Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))
set p = ( the Point of RAS,x) . W;
set p9m = ( the Point of RAS,v) . W;
consider p99m being Point of RAS such that
A3: p99m @ the Point of RAS = ((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W) by MIDSP_1:def_3;
A4: ( W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x & W . ( the Point of RAS,(( the Point of RAS,v) . W)) = v ) by Th15, MIDSP_2:33;
A5: W . ( the Point of RAS,p99m) = (W . ( the Point of RAS,((( the Point of RAS,x) . W) . m))) + (W . ( the Point of RAS,(( the Point of RAS,v) . W))) by A3, MIDSP_2:30
.= (x . m) + v by A4, Def9 ;
 (( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W
proof
set pp = (( the Point of RAS,x) . W) +* (m,p99m);
set xx = x +* (m,((x . m) + v));
set qq = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W;
 for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i
proof
let i be Nat of n; ::_thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i
percases ( i = m or i <> m ) ;
supposeA6: i = m ; ::_thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i
hence ((( the Point of RAS,x) . W) +* (m,p99m)) . i = p99m by Th10
.= ( the Point of RAS,((x . m) + v)) . W by A5, MIDSP_2:33
.= ( the Point of RAS,((x +* (m,((x . m) + v))) . m)) . W by Th13
.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by A6, Def8 ;
::_thesis: verum
end;
supposeA7: i <> m ; ::_thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i
hence ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,x) . W) . i by FUNCT_7:32
.= ( the Point of RAS,(x . i)) . W by Def8
.= ( the Point of RAS,((x +* (m,((x . m) + v))) . i)) . W by A7, FUNCT_7:32
.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by Def8 ;
::_thesis: verum
end;
end;
end;
hence  (( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W by Th9; ::_thesis: verum
end;
then A8: Phi (x +* (m,((x . m) + v))) = W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m))))) by Lm5;
A9: (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W
proof
set pp = (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W));
set qq = ( the Point of RAS,(x +* (m,v))) . W;
 for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i
proof
let i be Nat of n; ::_thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i
percases ( i = m or i <> m ) ;
supposeA10: i = m ; ::_thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i
hence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = ( the Point of RAS,v) . W by Th10
.= ( the Point of RAS,((x +* (m,v)) . m)) . W by Th13
.= (( the Point of RAS,(x +* (m,v))) . W) . i by A10, Def8 ;
::_thesis: verum
end;
supposeA11: i <> m ; ::_thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i
hence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,x) . W) . i by FUNCT_7:32
.= ( the Point of RAS,(x . i)) . W by Def8
.= ( the Point of RAS,((x +* (m,v)) . i)) . W by A11, FUNCT_7:32
.= (( the Point of RAS,(x +* (m,v))) . W) . i by Def8 ;
::_thesis: verum
end;
end;
end;
hence  (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W by Th9; ::_thesis: verum
end;
 ( RAS is_semi_additive_in m & *' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W))))) = (*' ( the Point of RAS,(( the Point of RAS,x) . W))) @ (*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))) ) by A1, A2, Def6, Th29;
then A12: W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m))))) = (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) + (W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))))) by A3, Lm6;
 Phi x = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W)))) by Lm5;
hence  Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) by A12, A8, A9, Lm5; ::_thesis: verum
end;
thus  ( ( 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))) ) implies RAS is_additive_in m ) ::_thesis: verum
proof
assume A13: 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))) ; ::_thesis: RAS is_additive_in m
then A14: RAS is_semi_additive_in m by Lm7;
 for a, pm, p9m being Point of RAS
for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
proof
let a, pm, p9m be Point of RAS; ::_thesis: for p being Tuple of (n + 1),RAS st p . m = pm holds
*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
let p be Tuple of (n + 1),RAS; ::_thesis: ( p . m = pm implies *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) )
assume A15: p . m = pm ; ::_thesis: *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))
set x = W . (a,p);
set v = W . (a,p9m);
consider p99m being Point of RAS such that
A16: p99m @ a = (p . m) @ p9m by MIDSP_1:def_3;
A17: (a,(W . (a,p))) . W = p by Th15;
A18: W . (a,p99m) = (W . (a,(p . m))) + (W . (a,p9m)) by A16, MIDSP_2:30
.= ((W . (a,p)) . m) + (W . (a,p9m)) by Def9 ;
 p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W
proof
set pp = p +* (m,p99m);
set xx = (W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))));
set qq = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W;
 for i being Nat of n holds (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
proof
let i be Nat of n; ::_thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
percases ( i = m or i <> m ) ;
supposeA19: i = m ; ::_thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
hence (p +* (m,p99m)) . i = p99m by Th10
.= (a,(((W . (a,p)) . m) + (W . (a,p9m)))) . W by A18, MIDSP_2:33
.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . m)) . W by Th13
.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by A19, Def8 ;
::_thesis: verum
end;
supposeA20: i <> m ; ::_thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i
hence (p +* (m,p99m)) . i = p . i by FUNCT_7:32
.= (a,((W . (a,p)) . i)) . W by A17, Def8
.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . i)) . W by A20, FUNCT_7:32
.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by Def8 ;
::_thesis: verum
end;
end;
end;
hence  p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W by Th9; ::_thesis: verum
end;
then A21: Phi ((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) = W . (a,(*' (a,(p +* (m,p99m))))) by Lm5;
A22: (a,(W . (a,p9m))) . W = p9m by MIDSP_2:33;
 p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W
proof
set pp = p +* (m,p9m);
set qq = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W;
 for i being Nat of n holds (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
proof
let i be Nat of n; ::_thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
percases ( i = m or i <> m ) ;
supposeA23: i = m ; ::_thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
hence (p +* (m,p9m)) . i = p9m by Th10
.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . m)) . W by A22, Th13
.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by A23, Def8 ;
::_thesis: verum
end;
supposeA24: i <> m ; ::_thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i
hence (p +* (m,p9m)) . i = p . i by FUNCT_7:32
.= (a,((W . (a,p)) . i)) . W by A17, Def8
.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . i)) . W by A24, FUNCT_7:32
.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by Def8 ;
::_thesis: verum
end;
end;
end;
hence  p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W by Th9; ::_thesis: verum
end;
then A25: Phi ((W . (a,p)) +* (m,(W . (a,p9m)))) = W . (a,(*' (a,(p +* (m,p9m))))) by Lm5;
 Phi (W . (a,p)) = W . (a,(*' (a,p))) by Lm4;
then  W . (a,(*' (a,(p +* (m,p99m))))) = (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m)))))) by A13, A21, A25;
hence  *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) by A14, A15, A16, Lm6; ::_thesis: verum
end;
hence  RAS is_additive_in m by Def6; ::_thesis: verum
end;
end;

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 & m <= n holds
W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m))
proof
let n be Element of NAT ; ::_thesis: 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))
let m be Nat of n; ::_thesis: 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))
let RAS be ReperAlgebra of n; ::_thesis: 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))
let a be Point of RAS; ::_thesis: 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))
let p be Tuple of (n + 1),RAS; ::_thesis: 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))
let W be ATLAS of RAS; ::_thesis: 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))
let x be Tuple of (n + 1),W; ::_thesis: ( W . (a,p) = x & m <= n implies W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m)) )
assume that
A1: W . (a,p) = x and
A2: m <= n ; ::_thesis: W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m))
reconsider m9 = m + 1 as Nat of n by A2, Th8;
set y = W . (a,(p +* (m9,(p . m))));
set z = x +* (m9,(x . m));
 for k being Nat of n holds (W . (a,(p +* (m9,(p . m))))) . k = (x +* (m9,(x . m))) . k
proof
let k be Nat of n; ::_thesis: (W . (a,(p +* (m9,(p . m))))) . k = (x +* (m9,(x . m))) . k
now__::_thesis:_(W_._(a,(p_+*_(m9,(p_._m)))))_._k_=_(x_+*_(m9,(x_._m)))_._k
percases ( k = m9 or k <> m9 ) ;
supposeA3: k = m9 ; ::_thesis: (W . (a,(p +* (m9,(p . m))))) . k = (x +* (m9,(x . m))) . k
thus (W . (a,(p +* (m9,(p . m))))) . k = W . (a,((p +* (m9,(p . m))) . k)) by Def9
.= W . (a,(p . m)) by A3, Th10
.= x . m by A1, Def9
.= (x +* (m9,(x . m))) . k by A3, Th13 ; ::_thesis: verum
end;
supposeA4: k <> m9 ; ::_thesis: (W . (a,(p +* (m9,(p . m))))) . k = (x +* (m9,(x . m))) . k
thus (W . (a,(p +* (m9,(p . m))))) . k = W . (a,((p +* (m9,(p . m))) . k)) by Def9
.= W . (a,(p . k)) by A4, FUNCT_7:32
.= x . k by A1, Def9
.= (x +* (m9,(x . m))) . k by A4, FUNCT_7:32 ; ::_thesis: verum
end;
end;
end;
hence  (W . (a,(p +* (m9,(p . m))))) . k = (x +* (m9,(x . m))) . k ; ::_thesis: verum
end;
hence  W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m)) by Th14; ::_thesis: verum
end;

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 & m <= n holds
(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))
proof
let n be Element of NAT ; ::_thesis: 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))
let m be Nat of n; ::_thesis: 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))
let RAS be ReperAlgebra of n; ::_thesis: 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))
let a be Point of RAS; ::_thesis: 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))
let p be Tuple of (n + 1),RAS; ::_thesis: 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))
let W be ATLAS of RAS; ::_thesis: 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))
let x be Tuple of (n + 1),W; ::_thesis: ( (a,x) . W = p & m <= n implies (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m)) )
assume that
A1: (a,x) . W = p and
A2: m <= n ; ::_thesis: (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))
 W . (a,p) = x by A1, Th15;
then  W . (a,(p +* ((m + 1),(p . m)))) = x +* ((m + 1),(x . m)) by A2, Th31;
hence  (a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m)) by Th15; ::_thesis: verum
end;

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 )
proof
let n be Element of NAT ; ::_thesis: 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 )
let m be Nat of n; ::_thesis: 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 )
let RAS be ReperAlgebra of n; ::_thesis: 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 )
let W be ATLAS of RAS; ::_thesis: ( m <= n implies ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) )
assume A1: m <= n ; ::_thesis: ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
thus  ( RAS is_alternative_in m implies for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) ::_thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) implies RAS is_alternative_in m )
proof
set a = the Point of RAS;
assume A2: RAS is_alternative_in m ; ::_thesis: for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W
let x be Tuple of (n + 1),W; ::_thesis: Phi (x +* ((m + 1),(x . m))) = 0. W
set p = ( the Point of RAS,x) . W;
set b = ( the Point of RAS,(0. W)) . W;
set p9 = (( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m));
 ( the Point of RAS,(0. W)) . W = the Point of RAS by MIDSP_2:34;
then A3: *' ( the Point of RAS,((( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m)))) = ( the Point of RAS,(0. W)) . W by A2, Def7;
 ( the Point of RAS,(x +* ((m + 1),(x . m)))) . W = (( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m)) by A1, Th32;
hence  Phi (x +* ((m + 1),(x . m))) = 0. W by A3, Th24; ::_thesis: verum
end;
assume A4: for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ; ::_thesis: RAS is_alternative_in m
 for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pm being Point of RAS st p . m = pm holds
*' (a,(p +* ((m + 1),pm))) = a
proof
let a be Point of RAS; ::_thesis: for p being Tuple of (n + 1),RAS
for pm being Point of RAS st p . m = pm holds
*' (a,(p +* ((m + 1),pm))) = a
let p be Tuple of (n + 1),RAS; ::_thesis: for pm being Point of RAS st p . m = pm holds
*' (a,(p +* ((m + 1),pm))) = a
let pm be Point of RAS; ::_thesis: ( p . m = pm implies *' (a,(p +* ((m + 1),pm))) = a )
assume A5: p . m = pm ; ::_thesis: *' (a,(p +* ((m + 1),pm))) = a
set x = W . (a,p);
set v = W . (a,a);
set x9 = (W . (a,p)) +* ((m + 1),((W . (a,p)) . m));
 W . (a,a) = 0. W by MIDSP_2:33;
then A6: Phi ((W . (a,p)) +* ((m + 1),((W . (a,p)) . m))) = W . (a,a) by A4;
 W . (a,(p +* ((m + 1),(p . m)))) = (W . (a,p)) +* ((m + 1),((W . (a,p)) . m)) by A1, Th31;
hence  *' (a,(p +* ((m + 1),pm))) = a by A5, A6, Th23; ::_thesis: verum
end;
hence  RAS is_alternative_in m by Def7; ::_thesis: verum
end;