:: MIDSP_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MIDSP_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, k being Nat
for D being non empty set
for p being FinSequence of D st len p = (j + 1) + k holds
ex q, r being FinSequence of D ex c being Element of D st
( len q = j & len r = k & p = (q ^ <*c*>) ^ r )
proof end;

theorem Th2: :: MIDSP_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i in Seg n holds
ex j, k being Nat st
( n = (j + 1) + k & i = j + 1 )
proof end;

theorem Th3: :: MIDSP_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for D being non empty set
for c being Element of D
for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds
( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )
proof end;

theorem Th4: :: MIDSP_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, j being Nat holds
( l <= j or l = j + 1 or j + 2 <= l )
proof end;

theorem Th5: :: MIDSP_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, n, i, j being Nat st l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) holds
( i + 1 <= l & l <= n )
proof end;

definition
let n, i be Nat;
let D be non empty set ;
let d be Element of D;
let p be Element of n -tuples_on D;
assume A1: i in Seg n ;
func sub p,i,d -> Element of n -tuples_on D means :Def1: :: MIDSP_3:def 1
( it . i = d & ( for l being Nat st l in (dom p) \ {i} holds
it . l = p . l ) );
existence
ex b1 being Element of n -tuples_on D st
( b1 . i = d & ( for l being Nat st l in (dom p) \ {i} holds
b1 . l = p . l ) )
proof end;
uniqueness
for b1, b2 being Element of n -tuples_on D st b1 . i = d & ( for l being Nat st l in (dom p) \ {i} holds
b1 . l = p . l ) & b2 . i = d & ( for l being Nat st l in (dom p) \ {i} holds
b2 . l = p . l ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines sub MIDSP_3:def 1 :
for n, i being Nat
for D being non empty set
for d being Element of D
for p being Element of n -tuples_on D st i in Seg n holds
for b6 being Element of n -tuples_on D holds
( b6 = sub p,i,d iff ( b6 . i = d & ( for l being Nat st l in (dom p) \ {i} holds
b6 . l = p . l ) ) );

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

registration
let n be Nat;
let A be non empty set ;
let m be BinOp of A;
let r be Function of n -tuples_on A,A;
cluster ReperAlgebraStr(# A,m,r #) -> non empty ;
coherence
not ReperAlgebraStr(# A,m,r #) is empty by STRUCT_0:def 1;
end;

Lm1: now
let n be Nat; :: thesis: for M being MidSp
for R being Function of (n + 2) -tuples_on the carrier of M,the carrier of M holds ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-like
let M be MidSp; :: thesis: for R being Function of (n + 2) -tuples_on the carrier of M,the carrier of M holds ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-like
let R be Function of (n + 2) -tuples_on the carrier of M,the carrier of M; :: thesis: ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-like
set RA = ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #);
thus ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) is MidSp-like :: thesis: verum
proof
let a, b, c, d be Element of ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #); :: according to MIDSP_1:def 4 :: 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 a' = a, b' = b, c' = c, d' = d as Element of M ;
A1: for a, b being Element of ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #)
for a', b' being Element of M st a = a' & b = b' holds
a @ b = a' @ b' ;
thus a @ a = a' @ a'
.= a by MIDSP_1:def 4 ; :: 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 )
thus a @ b = b' @ a' by A1
.= 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 )
( a @ b = a' @ b' & c @ d = c' @ d' & a' @ c' = a @ c & b' @ d' = b @ d ) by A1;
hence (a @ b) @ (c @ d) = (a' @ b') @ (c' @ d')
.= (a' @ c') @ (b' @ d') by MIDSP_1:def 4
.= (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
consider x' being Element of M such that
A2: x' @ a' = b' by MIDSP_1:def 4;
reconsider x = x' as Element of ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) ;
take x ; :: thesis: x @ a = b
thus x @ a = b by A2; :: thesis: verum
end;
end;

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

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

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

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of 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:118;
end;

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
let i, j be Nat;
let p be Tuple of i,RAS;
let q be Tuple of j,RAS;
:: original: ^
redefine func p ^ q -> Tuple of (i + j),RAS;
coherence
p ^ q is Tuple of (i + j),RAS by FINSEQ_2:127;
end;

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of 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 2
the reper of RAS . (<*a*> ^ p);
coherence
the reper of RAS . (<*a*> ^ p) is Point of RAS
proof end;
end;

:: deftheorem defines *' MIDSP_3:def 2 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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);

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
let d be Point of RAS;
let p be Tuple of (n + 1),RAS;
func <:p,i,d:> -> Tuple of (n + 1),RAS means :Def3: :: MIDSP_3:def 3
for D being non empty set
for p' being Element of (n + 1) -tuples_on D
for d' being Element of D st D = the carrier of RAS & p' = p & d' = d holds
it = sub p',i,d';
existence
ex b1 being Tuple of (n + 1),RAS st
for D being non empty set
for p' being Element of (n + 1) -tuples_on D
for d' being Element of D st D = the carrier of RAS & p' = p & d' = d holds
b1 = sub p',i,d'
proof end;
uniqueness
for b1, b2 being Tuple of (n + 1),RAS st ( for D being non empty set
for p' being Element of (n + 1) -tuples_on D
for d' being Element of D st D = the carrier of RAS & p' = p & d' = d holds
b1 = sub p',i,d' ) & ( for D being non empty set
for p' being Element of (n + 1) -tuples_on D
for d' being Element of D st D = the carrier of RAS & p' = p & d' = d holds
b2 = sub p',i,d' ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines <: MIDSP_3:def 3 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for d being Point of RAS
for p, b6 being Tuple of (n + 1),RAS holds
( b6 = <:p,i,d:> iff for D being non empty set
for p' being Element of (n + 1) -tuples_on D
for d' being Element of D st D = the carrier of RAS & p' = p & d' = d holds
b6 = sub p',i,d' );

theorem :: MIDSP_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: MIDSP_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for d being Point of RAS
for p being Tuple of (n + 1),RAS st i in Seg (n + 1) holds
( <:p,i,d:> . i = d & ( for l being Nat st l in (dom p) \ {i} holds
<:p,i,d:> . l = p . l ) )
proof end;

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

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

theorem Th8: :: MIDSP_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat holds
( i is Nat of n iff i in Seg (n + 1) )
proof end;

theorem :: MIDSP_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: MIDSP_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i <= n holds
i + 1 is Nat of n
proof end;

theorem Th11: :: MIDSP_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds p . m = q . m ) holds
p = q
proof end;

theorem Th12: :: MIDSP_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for d being Point of RAS
for p being Tuple of (n + 1),RAS holds
( ( for l being Nat of n st l = i holds
<:p,i,d:> . l = d ) & ( for l, i being Nat of n st l <> i holds
<:p,i,d:> . l = p . l ) )
proof end;

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

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
attr RAS is being_invariance means :Def5: :: MIDSP_3:def 5
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 Def5 defines being_invariance MIDSP_3:def 5 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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) );

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

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
pred RAS has_property_of_zero_in i means :Def6: :: MIDSP_3:def 6
for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' a,<:p,i,a:> = a;
end;

:: deftheorem Def6 defines has_property_of_zero_in MIDSP_3:def 6 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS has_property_of_zero_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' a,<:p,i,a:> = a );

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
pred RAS is_semi_additive_in i means :Def7: :: MIDSP_3:def 7
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 Def7 defines is_semi_additive_in MIDSP_3:def 7 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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 Th13: :: MIDSP_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for m being Nat of n st RAS is_semi_additive_in m holds
for a, d being Point of RAS
for p, q being Tuple of (n + 1),RAS st q = <:p,m,d:> holds
*' a,<:p,m,(a @ d):> = a @ (*' a,q)
proof end;

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
pred RAS is_additive_in i means :Def8: :: MIDSP_3:def 8
for a, pii, p'i being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' a,<:p,i,(pii @ p'i):> = (*' a,p) @ (*' a,<:p,i,p'i:>);
end;

:: deftheorem Def8 defines is_additive_in MIDSP_3:def 8 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS is_additive_in i iff for a, pii, p'i being Point of RAS
for p being Tuple of (n + 1),RAS st p . i = pii holds
*' a,<:p,i,(pii @ p'i):> = (*' a,p) @ (*' a,<:p,i,p'i:>) );

definition
let n, i be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
pred RAS is_alternative_in i means :Def9: :: MIDSP_3:def 9
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 Def9 defines is_alternative_in MIDSP_3:def 9 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2 holds
( RAS is_alternative_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pii being Point of RAS st p . i = pii holds
*' a,<:p,(i + 1),pii:> = a );

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

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
let W be ATLAS of RAS;
let x be Tuple of (n + 1),W;
let i be Nat;
let v be Vector of W;
func <:x,i,v:> -> Tuple of (n + 1),W means :Def10: :: MIDSP_3:def 10
for D being non empty set
for x' being Element of (n + 1) -tuples_on D
for v' being Element of D st D = the carrier of the algebra of W & x' = x & v' = v holds
it = sub x',i,v';
existence
ex b1 being Tuple of (n + 1),W st
for D being non empty set
for x' being Element of (n + 1) -tuples_on D
for v' being Element of D st D = the carrier of the algebra of W & x' = x & v' = v holds
b1 = sub x',i,v'
proof end;
uniqueness
for b1, b2 being Tuple of (n + 1),W st ( for D being non empty set
for x' being Element of (n + 1) -tuples_on D
for v' being Element of D st D = the carrier of the algebra of W & x' = x & v' = v holds
b1 = sub x',i,v' ) & ( for D being non empty set
for x' being Element of (n + 1) -tuples_on D
for v' being Element of D st D = the carrier of the algebra of W & x' = x & v' = v holds
b2 = sub x',i,v' ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines <: MIDSP_3:def 10 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for x being Tuple of (n + 1),W
for i being Nat
for v being Vector of W
for b7 being Tuple of (n + 1),W holds
( b7 = <:x,i,v:> iff for D being non empty set
for x' being Element of (n + 1) -tuples_on D
for v' being Element of D st D = the carrier of the algebra of W & x' = x & v' = v holds
b7 = sub x',i,v' );

theorem Th14: :: MIDSP_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st i in Seg (n + 1) holds
( <:x,i,v:> . i = v & ( for l being Nat st l in (dom x) \ {i} holds
<:x,i,v:> . l = x . l ) )
proof end;

theorem Th15: :: MIDSP_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W holds
( ( for l being Nat of n st l = i holds
<:x,i,v:> . l = v ) & ( for l, i being Nat of n st l <> i holds
<:x,i,v:> . l = x . l ) )
proof end;

theorem Th16: :: MIDSP_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds
x = y
proof end;

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

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of 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 :Def11: :: MIDSP_3:def 11
for m being Nat of n holds it . m = a,(x . m) . W;
existence
ex b1 being Tuple of (n + 1),RAS st
for m being Nat of n holds b1 . m = a,(x . m) . W
proof end;
uniqueness
for b1, b2 being Tuple of (n + 1),RAS st ( for m being Nat of n holds b1 . m = a,(x . m) . W ) & ( for m being Nat of n holds b2 . m = a,(x . m) . W ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines . MIDSP_3:def 11 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS
for a being Point of RAS
for x being Tuple of (n + 1),W
for b6 being Tuple of (n + 1),RAS holds
( b6 = a,x . W iff for m being Nat of n holds b6 . m = a,(x . m) . W );

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2;
let W be ATLAS of RAS;
let a be Point of RAS;
let p be Tuple of (n + 1),RAS;
func W . a,p -> Tuple of (n + 1),W means :Def12: :: MIDSP_3:def 12
for m being Nat of n holds it . m = W . a,(p . m);
existence
ex b1 being Tuple of (n + 1),W st
for m being Nat of n holds b1 . m = W . a,(p . m)
proof end;
uniqueness
for b1, b2 being Tuple of (n + 1),W st ( for m being Nat of n holds b1 . m = W . a,(p . m) ) & ( for m being Nat of n holds b2 . m = W . a,(p . m) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines . MIDSP_3:def 12 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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 Th17: :: MIDSP_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . a,p = x iff a,x . W = p )
proof end;

theorem :: MIDSP_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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 Th17;

theorem :: MIDSP_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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 Th17;

definition
let n be Nat;
let RAS be non empty MidSp-like ReperAlgebraStr of 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 13
W . a,(*' a,(a,x . W));
coherence
W . a,(*' a,(a,x . W)) is Vector of W ;
end;

:: deftheorem defines Phi MIDSP_3:def 13 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of 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 Th20: :: MIDSP_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . a,p = x & W . a,b = v holds
( *' a,p = b iff Phi a,x = v )
proof end;

theorem Th21: :: MIDSP_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for W being ATLAS of RAS holds
( RAS is_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi a,x = Phi b,x )
proof end;

theorem Th22: :: MIDSP_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds 1 in Seg (n + 1)
proof end;

theorem :: MIDSP_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: MIDSP_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds 1 is Nat of n
proof end;

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

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

theorem Th25: :: MIDSP_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi a,x = Phi b,x
proof end;

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

:: deftheorem Def15 defines Phi MIDSP_3:def 15 :
for n being Nat
for RAS being ReperAlgebra of n
for W being ATLAS of RAS
for x being Tuple of (n + 1),W
for b5 being Vector of W holds
( b5 = Phi x iff for a being Point of RAS holds b5 = Phi a,x );

Lm2: for n being Nat
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st W . a,p = x holds
Phi x = W . a,(*' a,p)
proof end;

Lm3: for n being Nat
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st a,x . W = p holds
Phi x = W . a,(*' a,p)
proof end;

theorem Th26: :: MIDSP_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . a,p = x & W . a,b = v & Phi x = v holds
*' a,p = b
proof end;

theorem Th27: :: MIDSP_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st a,x . W = p & a,v . W = b & *' a,p = b holds
Phi x = v
proof end;

theorem Th28: :: MIDSP_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . a,p = x & W . a,b = v holds
W . a,<:p,m,b:> = <:x,m,v:>
proof end;

theorem Th29: :: MIDSP_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st a,x . W = p & a,v . W = b holds
a,<:x,m,v:> . W = <:p,m,b:>
proof end;

theorem :: MIDSP_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi <:x,m,(0. W):> = 0. W )
proof end;

theorem Th31: :: MIDSP_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS is_semi_additive_in m iff for x being Tuple of (n + 1),W holds Phi <:x,m,(Double (x . m)):> = Double (Phi x) )
proof end;

theorem Th32: :: MIDSP_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n st RAS has_property_of_zero_in m & RAS is_additive_in m holds
RAS is_semi_additive_in m
proof end;

Lm4: for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS is_semi_additive_in m holds
for a, p'm, p''m being Point of RAS
for p being Tuple of (n + 1),RAS st a @ p''m = (p . m) @ p'm holds
( *' a,<:p,m,((p . m) @ p'm):> = (*' a,p) @ (*' a,<:p,m,p'm:>) iff W . a,(*' a,<:p,m,p''m:>) = (W . a,(*' a,p)) + (W . a,(*' a,<:p,m,p'm:>)) )
proof end;

Lm5: for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st ( for x being Tuple of (n + 1),W
for v being Vector of W holds Phi <:x,m,((x . m) + v):> = (Phi x) + (Phi <:x,m,v:>) ) holds
RAS is_semi_additive_in m
proof end;

theorem :: MIDSP_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st RAS has_property_of_zero_in m holds
( RAS is_additive_in m iff for x being Tuple of (n + 1),W
for v being Vector of W holds Phi <:x,m,((x . m) + v):> = (Phi x) + (Phi <:x,m,v:>) )
proof end;

theorem Th34: :: MIDSP_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st W . a,p = x & m <= n holds
W . a,<:p,(m + 1),(p . m):> = <:x,(m + 1),(x . m):>
proof end;

theorem Th35: :: MIDSP_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st a,x . W = p & m <= n holds
a,<:x,(m + 1),(x . m):> . W = <:p,(m + 1),(p . m):>
proof end;

theorem :: MIDSP_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st m <= n holds
( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi <:x,(m + 1),(x . m):> = 0. W )
proof end;