:: Oriented Metric-Affine Plane - Part I
:: by Jaroslaw Zajkowski
::
:: Received October 24, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

Lm1:  for V being RealLinearSpace
for v1, x, y, v2 being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * x) + (b2 * y) & v2 = (c1 * x) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) )
proofend;

Lm2:  for V being RealLinearSpace
for v, x, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
proofend;

Lm3:  for V being RealLinearSpace
for x, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen x,y & (a1 * x) + (a2 * y) = (b1 * x) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
proofend;

Lm4:  for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
( x <> 0. V &amp; y <> 0. V )
proofend;

Lm5:  for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)
proofend;

Lm6:  for V being RealLinearSpace
for x, y, u being VECTOR of V
for k1, k2 being Real st Gen x,y &amp; u = (k1 * x) + (k2 * y) holds
( k1 = pr1 (x,y,u) &amp; k2 = pr2 (x,y,u) )
proofend;

Lm7:  for V being RealLinearSpace
for x, y, u, v being VECTOR of V
for a being Real st Gen x,y holds
( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) &amp; pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) &amp; pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) &amp; pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) &amp; pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) &amp; pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
proofend;

definition
let V be RealLinearSpace;
let x, y, u be VECTOR of V;
func Ortm (x,y,u) ->  VECTOR of V equals :: ANALORT:def 1
((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y);
correctness
coherence
((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y) is VECTOR of V;
;
end;

:: deftheorem  defines Ortm ANALORT:def_1_:_
 for V being RealLinearSpace
for x, y, u being VECTOR of V holds Ortm (x,y,u) = ((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y);

theorem Th1: :: ANALORT:1
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Ortm (x,y,(u + v)) = (Ortm (x,y,u)) + (Ortm (x,y,v))
proofend;

theorem Th2: :: ANALORT:2
for V being RealLinearSpace
for x, y, u being VECTOR of V
for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
proofend;

theorem :: ANALORT:3
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
Ortm (x,y,(0. V)) = 0. V
proofend;

theorem Th4: :: ANALORT:4
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
Ortm (x,y,(- u)) = - (Ortm (x,y,u))
proofend;

theorem Th5: :: ANALORT:5
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v))
proofend;

theorem Th6: :: ANALORT:6
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y &amp; Ortm (x,y,u) = Ortm (x,y,v) holds
u = v
proofend;

theorem Th7: :: ANALORT:7
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
Ortm (x,y,(Ortm (x,y,u))) = u
proofend;

theorem Th8: :: ANALORT:8
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
ex v being VECTOR of V st u = Ortm (x,y,v)
proofend;

definition
let V be RealLinearSpace;
let x, y, u be VECTOR of V;
func Orte (x,y,u) ->  VECTOR of V equals :: ANALORT:def 2
((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y);
correctness
coherence
((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y) is VECTOR of V;
;
end;

:: deftheorem  defines Orte ANALORT:def_2_:_
 for V being RealLinearSpace
for x, y, u being VECTOR of V holds Orte (x,y,u) = ((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y);

theorem Th9: :: ANALORT:9
for V being RealLinearSpace
for x, y, v being VECTOR of V st Gen x,y holds
Orte (x,y,(- v)) = - (Orte (x,y,v))
proofend;

theorem Th10: :: ANALORT:10
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v))
proofend;

theorem Th11: :: ANALORT:11
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v))
proofend;

theorem Th12: :: ANALORT:12
for V being RealLinearSpace
for x, y, u being VECTOR of V
for n being Real st Gen x,y holds
Orte (x,y,(n * u)) = n * (Orte (x,y,u))
proofend;

theorem Th13: :: ANALORT:13
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y &amp; Orte (x,y,u) = Orte (x,y,v) holds
u = v
proofend;

theorem Th14: :: ANALORT:14
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
Orte (x,y,(Orte (x,y,u))) = - u
proofend;

theorem Th15: :: ANALORT:15
for V being RealLinearSpace
for x, y, u being VECTOR of V st Gen x,y holds
ex v being VECTOR of V st Orte (x,y,v) = u
proofend;

definition
let V be RealLinearSpace;
let x, y, u, v, u1, v1 be VECTOR of V;
predu,v,u1,v1 are_COrte_wrt x,y means :Def3: :: ANALORT:def 3
 Orte (x,y,u), Orte (x,y,v) // u1,v1;
predu,v,u1,v1 are_COrtm_wrt x,y means :Def4: :: ANALORT:def 4
 Ortm (x,y,u), Ortm (x,y,v) // u1,v1;
end;

:: deftheorem Def3 defines are_COrte_wrt ANALORT:def_3_:_
 for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_COrte_wrt x,y iff Orte (x,y,u), Orte (x,y,v) // u1,v1 );

:: deftheorem Def4 defines are_COrtm_wrt ANALORT:def_4_:_
 for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_COrtm_wrt x,y iff Ortm (x,y,u), Ortm (x,y,v) // u1,v1 );

theorem Th16: :: ANALORT:16
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y &amp; u,v // u1,v1 holds
Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
proofend;

theorem Th17: :: ANALORT:17
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y &amp; u,v // u1,v1 holds
Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
proofend;

theorem Th18: :: ANALORT:18
for V being RealLinearSpace
for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrte_wrt x,y holds
v,v1,u1,u are_COrte_wrt x,y
proofend;

theorem Th19: :: ANALORT:19
for V being RealLinearSpace
for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrtm_wrt x,y holds
v,v1,u,u1 are_COrtm_wrt x,y
proofend;

theorem Th20: :: ANALORT:20
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y
proofend;

theorem :: ANALORT:21
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrtm_wrt x,y
proofend;

theorem :: ANALORT:22
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrte_wrt x,y
proofend;

theorem :: ANALORT:23
for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrtm_wrt x,y
proofend;

theorem Th24: :: ANALORT:24
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y holds
u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y
proofend;

theorem :: ANALORT:25
for V being RealLinearSpace
for u, v, x, y being VECTOR of V holds u,v, Orte (x,y,u), Orte (x,y,v) are_COrte_wrt x,y
proofend;

theorem :: ANALORT:26
for V being RealLinearSpace
for u, v, x, y being VECTOR of V holds u,v, Ortm (x,y,u), Ortm (x,y,v) are_COrtm_wrt x,y
proofend;

theorem :: ANALORT:27
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 &amp; u2,v2,u,v are_COrte_wrt x,y &amp; u2,v2,u1,v1 are_COrte_wrt x,y ) )
proofend;

theorem :: ANALORT:28
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 &amp; u2,v2,u,v are_COrtm_wrt x,y &amp; u2,v2,u1,v1 are_COrtm_wrt x,y ) )
proofend;

theorem :: ANALORT:29
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y holds
( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) )
proofend;

theorem :: ANALORT:30
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y &amp; u,v,u1,v1 are_COrte_wrt x,y &amp; u,v,v1,u1 are_COrte_wrt x,y &amp; not u = v holds
u1 = v1
proofend;

theorem :: ANALORT:31
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y &amp; u,v,u1,v1 are_COrtm_wrt x,y &amp; u,v,v1,u1 are_COrtm_wrt x,y &amp; not u = v holds
u1 = v1
proofend;

theorem :: ANALORT:32
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y &amp; u,v,u1,v1 are_COrte_wrt x,y &amp; u,v,u1,w are_COrte_wrt x,y &amp; not u,v,v1,w are_COrte_wrt x,y holds
u,v,w,v1 are_COrte_wrt x,y
proofend;

theorem :: ANALORT:33
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y &amp; u,v,u1,v1 are_COrtm_wrt x,y &amp; u,v,u1,w are_COrtm_wrt x,y &amp; not u,v,v1,w are_COrtm_wrt x,y holds
u,v,w,v1 are_COrtm_wrt x,y
proofend;

theorem :: ANALORT:34
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V st u,v,u1,v1 are_COrte_wrt x,y holds
v,u,v1,u1 are_COrte_wrt x,y
proofend;

theorem :: ANALORT:35
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V st u,v,u1,v1 are_COrtm_wrt x,y holds
v,u,v1,u1 are_COrtm_wrt x,y
proofend;

theorem :: ANALORT:36
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y &amp; u,v,u1,v1 are_COrte_wrt x,y &amp; u,v,v1,w are_COrte_wrt x,y holds
u,v,u1,w are_COrte_wrt x,y
proofend;

theorem :: ANALORT:37
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y &amp; u,v,u1,v1 are_COrtm_wrt x,y &amp; u,v,v1,w are_COrtm_wrt x,y holds
u,v,u1,w are_COrtm_wrt x,y
proofend;

theorem :: ANALORT:38
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 &amp; w,u1,u,v are_COrte_wrt x,y )
proofend;

theorem :: ANALORT:39
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 &amp; w,u1,u,v are_COrtm_wrt x,y )
proofend;

theorem Th40: :: ANALORT:40
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 &amp; u,v,w,u1 are_COrte_wrt x,y )
proofend;

theorem Th41: :: ANALORT:41
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 &amp; u,v,w,u1 are_COrtm_wrt x,y )
proofend;

theorem :: ANALORT:42
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrte_wrt x,y &amp; w,w1,v,v1 are_COrte_wrt x,y &amp; w,w1,u2,v2 are_COrte_wrt x,y &amp; not w = w1 &amp; not v = v1 holds
u,u1,u2,v2 are_COrte_wrt x,y
proofend;

theorem :: ANALORT:43
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrtm_wrt x,y &amp; w,w1,v,v1 are_COrtm_wrt x,y &amp; w,w1,u2,v2 are_COrtm_wrt x,y &amp; not w = w1 &amp; not v = v1 holds
u,u1,u2,v2 are_COrtm_wrt x,y
proofend;

theorem :: ANALORT:44
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrte_wrt x,y &amp; v,v1,w,w1 are_COrte_wrt x,y &amp; u2,v2,w,w1 are_COrte_wrt x,y &amp; not u,u1,u2,v2 are_COrte_wrt x,y &amp; not v = v1 holds
w = w1
proofend;

theorem :: ANALORT:45
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrtm_wrt x,y &amp; v,v1,w,w1 are_COrtm_wrt x,y &amp; u2,v2,w,w1 are_COrtm_wrt x,y &amp; not u,u1,u2,v2 are_COrtm_wrt x,y &amp; not v = v1 holds
w = w1
proofend;

theorem :: ANALORT:46
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrte_wrt x,y &amp; v,v1,w,w1 are_COrte_wrt x,y &amp; u,u1,u2,v2 are_COrte_wrt x,y &amp; not u2,v2,w,w1 are_COrte_wrt x,y &amp; not v = v1 holds
u = u1
proofend;

theorem :: ANALORT:47
for V being RealLinearSpace
for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y &amp; u,u1,v,v1 are_COrtm_wrt x,y &amp; v,v1,w,w1 are_COrtm_wrt x,y &amp; u,u1,u2,v2 are_COrtm_wrt x,y &amp; not u2,v2,w,w1 are_COrtm_wrt x,y &amp; not v = v1 holds
u = u1
proofend;

theorem :: ANALORT:48
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y &amp; not v,v1,u1,w are_COrte_wrt x,y &amp; u1,w1,u1,w are_COrte_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) &amp; ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
proofend;

theorem :: ANALORT:49
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y &amp; ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y &amp; not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
proofend;

theorem :: ANALORT:50
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrtm_wrt x,y &amp; not v,v1,u1,w are_COrtm_wrt x,y &amp; u1,w1,u1,w are_COrtm_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) &amp; ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
proofend;

theorem :: ANALORT:51
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y &amp; ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y &amp; not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
proofend;

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CORTE (V,x,y) ->  Relation of [: the carrier of V, the carrier of V:] means :Def5: :: ANALORT:def 5
 for uu, vv being set holds
( [uu,vv] in it iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrte_wrt x,y ) );
existence
 ex b1 being Relation of [: the carrier of V, the carrier of V:] st
for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrte_wrt x,y ) )
proofend;
uniqueness
 for b1, b2 being Relation of [: the carrier of V, the carrier of V:] st ( for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) &amp; ( for uu, vv being set holds
( [uu,vv] in b2 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines CORTE ANALORT:def_5_:_
 for V being RealLinearSpace
for x, y being VECTOR of V
for b4 being Relation of [: the carrier of V, the carrier of V:] holds
( b4 = CORTE (V,x,y) iff for uu, vv being set holds
( [uu,vv] in b4 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrte_wrt x,y ) ) );

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CORTM (V,x,y) ->  Relation of [: the carrier of V, the carrier of V:] means :Def6: :: ANALORT:def 6
 for uu, vv being set holds
( [uu,vv] in it iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrtm_wrt x,y ) );
existence
 ex b1 being Relation of [: the carrier of V, the carrier of V:] st
for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrtm_wrt x,y ) )
proofend;
uniqueness
 for b1, b2 being Relation of [: the carrier of V, the carrier of V:] st ( for uu, vv being set holds
( [uu,vv] in b1 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) &amp; ( for uu, vv being set holds
( [uu,vv] in b2 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines CORTM ANALORT:def_6_:_
 for V being RealLinearSpace
for x, y being VECTOR of V
for b4 being Relation of [: the carrier of V, the carrier of V:] holds
( b4 = CORTM (V,x,y) iff for uu, vv being set holds
( [uu,vv] in b4 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] &amp; vv = [v1,v2] &amp; u1,u2,v1,v2 are_COrtm_wrt x,y ) ) );

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CESpace (V,x,y) ->  strict AffinStruct  equals :: ANALORT:def 7
 AffinStruct(# the carrier of V,(CORTE (V,x,y)) #);
correctness
coherence
AffinStruct(# the carrier of V,(CORTE (V,x,y)) #) is strict AffinStruct ;
;
end;

:: deftheorem  defines CESpace ANALORT:def_7_:_
 for V being RealLinearSpace
for x, y being VECTOR of V holds CESpace (V,x,y) = AffinStruct(# the carrier of V,(CORTE (V,x,y)) #);

registration
let V be RealLinearSpace;
let x, y be VECTOR of V;
cluster CESpace (V,x,y) ->  non empty strict ;
coherence
 not CESpace (V,x,y) is empty ;
end;

definition
let V be RealLinearSpace;
let x, y be VECTOR of V;
func CMSpace (V,x,y) ->  strict AffinStruct  equals :: ANALORT:def 8
 AffinStruct(# the carrier of V,(CORTM (V,x,y)) #);
correctness
coherence
AffinStruct(# the carrier of V,(CORTM (V,x,y)) #) is strict AffinStruct ;
;
end;

:: deftheorem  defines CMSpace ANALORT:def_8_:_
 for V being RealLinearSpace
for x, y being VECTOR of V holds CMSpace (V,x,y) = AffinStruct(# the carrier of V,(CORTM (V,x,y)) #);

registration
let V be RealLinearSpace;
let x, y be VECTOR of V;
cluster CMSpace (V,x,y) ->  non empty strict ;
coherence
 not CMSpace (V,x,y) is empty ;
end;

theorem :: ANALORT:52
for V being RealLinearSpace
for x, y being VECTOR of V
for uu being set holds
( uu is Element of (CESpace (V,x,y)) iff uu is VECTOR of V ) ;

theorem :: ANALORT:53
for V being RealLinearSpace
for x, y being VECTOR of V
for uu being set holds
( uu is Element of (CMSpace (V,x,y)) iff uu is VECTOR of V ) ;

theorem :: ANALORT:54
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CESpace (V,x,y)) st u = p &amp; v = q &amp; u1 = r &amp; v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
proofend;

theorem :: ANALORT:55
for V being RealLinearSpace
for u, v, u1, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p &amp; v = q &amp; u1 = r &amp; v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
proofend;