The Mizar article:

A Construction of Analytical Ordered Trapezium Spaces

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

Received October 29, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: GEOMTRAP
[ MML identifier index ]


environ

 vocabulary RLVECT_1, PARSP_1, ANALOAF, ANALMETR, DIRAF, ARYTM_1, TDGROUP,
      RELAT_1, SYMSP_1, FUNCT_3, BINOP_1, FUNCT_1, MIDSP_1, GEOMTRAP;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, REAL_1, STRUCT_0,
      DIRAF, RELSET_1, RLVECT_1, MIDSP_1, AFF_1, ANALOAF, BINOP_1, ANALMETR;
 constructors DOMAIN_1, REAL_1, MIDSP_1, AFF_1, BINOP_1, ANALMETR, XREAL_0,
      MEMBERED, XBOOLE_0;
 clusters SUBSET_1, DIRAF, ANALOAF, ANALMETR, RELSET_1, STRUCT_0, MEMBERED,
      ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions STRUCT_0;
 theorems RLVECT_1, RELAT_1, DIRAF, ANALOAF, SQUARE_1, ANALMETR, AFF_1,
      ZFMISC_1, RLSUB_2, VECTSP_1, XCMPLX_0, XCMPLX_1;
 schemes RELSET_1, BINOP_1, COMPLSP1;

begin

reserve V for RealLinearSpace;
reserve u,u1,u2,v,v1,v2,w,w1,y for VECTOR of V;
reserve a,a1,a2,b,b1,b2,c,c1,c2 for Real;
reserve x,z for set;

definition let V; let u,v,u1,v1;
  pred u,v '||' u1,v1 means :Def1:
  u,v // u1,v1 or u,v // v1,u1;
end;

theorem Th1: Gen w,y implies OASpace(V) is OAffinSpace
 proof assume Gen w,y; then for a1,a2 st a1*w + a2*y = 0.V holds
 a1=0 & a2=0 by ANALMETR:def 1; hence thesis by ANALOAF:38; end;

theorem Th2: for p,q,p1,q1 being Element of OASpace(V)
 st p=u & q=v & p1=u1 & q1=v1 holds (p,q // p1,q1 iff u,v // u1,v1)
 proof let p,q,p1,q1 be Element of OASpace(V) such that
 A1: p=u & q=v & p1=u1 & q1=v1; A2: OASpace(V) = AffinStruct
 (#the carrier of V, DirPar(V)#) by ANALOAF:def 4;
 A3: now assume p,q // p1,q1; then [[u,v],[u1,v1]] in
 DirPar(V) by A1,A2,ANALOAF:def 2;
  hence u,v // u1,v1 by ANALOAF:33; end;
    now assume u,v // u1,v1;
  then [[p,q],[p1,q1]] in the CONGR of OASpace(V) by A1,A2,ANALOAF:33;
  hence p,q // p1,q1 by ANALOAF:def 2; end;
hence thesis by A3; end;

theorem Th3: Gen w,y implies
 for p,q,p1,q1 being Element of (the carrier of Lambda(OASpace(V)))
 st p=u & q=v & p1=u1 & q1=v1 holds (p,q // p1,q1 iff u,v '||' u1,v1)
proof assume A1: Gen w,y; let p,q,p1,q1 be Element of
(the carrier of Lambda(OASpace(V))) such that A2: p=u & q=v & p1=u1 & q1=v1;
 reconsider S = OASpace(V) as OAffinSpace by A1,Th1;
   Lambda(OASpace(V)) = AffinStruct (# the carrier of OASpace(V),
 lambda(the CONGR of OASpace(V)) #) by DIRAF:def 2;
 then reconsider p'=p,q'=q,p1'=p1,q1'=q1 as Element of S;
 A3: now assume p,q // p1,q1; then p',q' '||' p1',q1' by DIRAF:45;
  then p',q' // p1',q1' or p',q' // q1',p1' by DIRAF:def 4; then u,v // u1,v1
or
  u,v // v1,u1 by A2,Th2; hence u,v '||' u1,v1 by Def1; end;
    now assume u,v '||' u1,v1; then u,v // u1,v1 or u,v // v1,u1 by Def1;
  then p',q' // p1',q1' or p',q' // q1',p1' by A2,Th2; then p',q' '||' p1',
q1'
  by DIRAF:def 4; hence p,q // p1,q1 by DIRAF:45; end;
hence thesis by A3; end;

theorem Th4:
 for p,q,p1,q1 being Element of (the carrier of AMSpace(V,w,y))
 st p=u & q=v & p1=u1 & q1=v1 holds (p,q // p1,q1 iff u,v '||' u1,v1)
proof let p,q,p1,q1 be Element of
(the carrier of AMSpace(V,w,y)) such that A1: p=u & q=v & p1=u1 & q1=v1;
A2: now assume u,v '||' u1,v1; then u,v // u1,v1 or u,v // v1,u1 by Def1;
 then ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by ANALMETR:18
; hence p,q // p1,q1 by A1,ANALMETR:32; end;
   now assume p,q // p1,q1; then ex a,b st
 a*(v-u) = b*(v1-u1) & (a<>0 or b<>0) by A1,ANALMETR:32;
then u,v // u1,v1 or
 u,v // v1,u1 by ANALMETR:18; hence u,v '||' u1,v1 by Def1; end;
hence thesis by A2; end;

definition let V; let u,v;
  func u#v -> VECTOR of V means :Def2:
  it+it = u+v;
existence proof set y = u+v; set w = (2")*y;
   2" + 2" = 1;
 then w+w = 1*y by RLVECT_1:def 9 .= y by RLVECT_1:def 9; hence thesis; end;
uniqueness proof let w,w1 such that A1: w+w = u+v and A2:w1+w1 = u+v;
   0.V = (w+w)-(w1+w1) by A1,A2,RLVECT_1:28
 .= w+(w-(w1+w1)) by RLVECT_1:42 .= w+((w-w1)-w1) by RLVECT_1:41
 .= (w+(w-w1))-w1 by RLVECT_1:42
 .= (w-w1)+(w-w1) by RLVECT_1:42; then w-w1 = 0.V by RLVECT_1:34;
 hence w=w1 by RLVECT_1:35; end;
 commutativity;
 idempotence;
end;

canceled 2;

theorem Th7: ex y st u#y=w proof take y = (-u)+(w+w);
   u+y = (u+(-u))+(w+w) by RLVECT_1:def 6 .= 0.V+(w+w)
 by RLVECT_1:16 .= w+w by RLVECT_1:10; hence u#y = w by Def2; end;

theorem Th8: (u#u1)#(v#v1)=(u#v)#(u1#v1)
 proof set p=u#u1, q=v#v1, r=u#v, s=u1#v1;
  set x=p#q,y=r#s;
  A1: (x+x)+(x+x) = (x+x)+(p+q) by Def2
   .= (p+q)+(p+q) by Def2 .= p+(q+(p+q)) by RLVECT_1:def 6
   .= p+(p+(q+q)) by RLVECT_1:def 6 .= (p+p)+(q+q)
   by RLVECT_1:def 6 .= (p+p)+(v+v1) by Def2 .= (u+u1)+(v+v1) by Def2
 .= u+(u1+(v+v1))
   by RLVECT_1:def 6 .= u+(v+(v1+u1)) by RLVECT_1:def 6
   .= (u+v)+(v1+u1) by RLVECT_1:def 6
   .= (u+v)+(s+s) by Def2 .= (r+r)+(s+s) by Def2
 .= r+(r+(s+s)) by RLVECT_1:def 6
   .= r+(s+(s+r)) by RLVECT_1:def 6 .= (r+s)+(s+r)
   by RLVECT_1:def 6 .= (y+y)+(r+s) by Def2
   .= (y+y)+(y+y) by Def2;
  A2: now let w; w=1*w by RLVECT_1:def 9; then (w+w)+(w+w) =
(1+1)*w + ((1*w)+(1*w)) by RLVECT_1:def 9
   .= (1+1)*w + (1+1)*w by RLVECT_1:def 9 .= ((1+1)+(1+1))*w by RLVECT_1:def 9;
 hence (w+w)+(w+w) = 4*w; end; then 4*x = (y+y)+(y+y) by A1 .= 4*y by A2;
 hence x=y by RLVECT_1:50; end;

theorem Th9: u#y=u#w implies y=w
 proof assume A1: u#y=u#w; set p=u#y;
   u+y = p+p by Def2 .= u+w by A1,Def2; hence y=w by RLVECT_1:21; end;

theorem Th10: u,v // y#u,y#v
proof set p=y#u,r=y#v; A1: y+u = p+p & y+v = r+r by Def2;
   2*(r-p) = (1+1)*r - (1+1)*p by RLVECT_1:48
 .= (1*r+1*r)-(1+1)*p by RLVECT_1:def 9 .= (1*r+1*r)-(1*p+1*p) by RLVECT_1:def
9
 .= (r+1*r)-(1*p+1*p) by RLVECT_1:def 9 .= (r+r)-(1*p+1*p) by RLVECT_1:def 9
 .= (r+r)-(p+1*p) by RLVECT_1:def 9 .= (y+v)-(y+u) by A1,RLVECT_1:def 9
 .= v+(y-(y+u)) by RLVECT_1:42 .= v+((y-y)-u) by RLVECT_1:41 .= v+(0.V-u)
 by RLVECT_1:28 .= v+(-u) by RLVECT_1:27 .= v-u by RLVECT_1:def 11 .= 1*(v-u)
 by RLVECT_1:def 9; hence u,v // p,r by ANALOAF:def 1; end;

theorem u,v '||' w#u,w#v
  proof u,v // w#u,w#v by Th10; hence thesis by Def1; end;

theorem Th12:
  2*(u#v-u) = v-u & 2*(v-u#v) = v-u
 proof set p=u#v;
 A1: 2-1 =1;
 A2: 1-2 = -1;
A3: 2*(p-u) = (1+1)*p - 2*u by RLVECT_1:48 .= (1*p+1*p) - 2*u
 by RLVECT_1:def 9 .= (p+1*p) - 2*u by RLVECT_1:def 9
 .= (p+p) - 2*u by RLVECT_1:def 9
 .= (u+v) - 2*u by Def2
 .=v+(u-2*u) by RLVECT_1:42
 .= v+(1*u-2*u) by RLVECT_1:def 9 .= v+(-1)*u by A2,RLVECT_1:49
 .= v+(-u) by RLVECT_1:29 .= v-u by RLVECT_1:def 11;
   2*(v-p) = 2*v-(1+1)*p by RLVECT_1:48 .= 2*v-(1*p+1*p) by RLVECT_1:def 9
 .= 2*v - (1*p+p) by RLVECT_1:def 9 .= 2*v - (p+p) by RLVECT_1:def 9
 .= 2*v - (u+v) by Def2
 .= (2*v-v)-u by RLVECT_1:41
 .= (2*v-1*v)-u by RLVECT_1:def 9 .= 1*v - u by A1,RLVECT_1:49
 .= v-u by RLVECT_1:def 9; hence thesis by A3; end;

theorem Th13: u,u#v // u#v,v proof set p = u#v;
  2*(p-u) = v-u by Th12 .= 2*(v-p) by Th12; hence thesis by ANALOAF:def 1; end
;

theorem Th14: u,v // u,u#v & u,v // u#v,v proof set p = u#v;
   1*(v-u) = v-u by RLVECT_1:def 9 .= 2*(p-u) by Th12;
 hence u,v // u,u#v by ANALOAF:def 1
; 1*(v-u) = v-u by RLVECT_1:def 9 .= 2*(v-p)
 by Th12; hence u,v // u#v,v by ANALOAF:def 1; end;

Lm1: u,y // y,v implies v,y // y,u & u,y // u,v & y,v // u,v
proof assume A1: u,y // y,v; then y,u // v,y by ANALOAF:21; hence
A2: v,y // y,u by ANALOAF:21; thus u,y // u,v by A1,ANALOAF:22;
  v,y // v,u by A2,ANALOAF:22; hence y,v // u,v by ANALOAF:21; end;

theorem Th15: u,y // y,v implies u#y,y // y,y#v
 proof assume A1: u,y // y,v; set p=u#y, q=y#v;
   u,p // p,y & y,q // q,v by Th13; then p,y // u,y & y,q // y,v by Lm1;
 then A2: u,y // p,y & y,v // y,q by ANALOAF:21;
   now assume that A3: u<>y and A4: y<>v;
   y,v // p,y by A1,A2,A3,ANALOAF:20; hence thesis by A2,A4,ANALOAF:20; end;
hence thesis by ANALOAF:18; end;

theorem Th16: u,v // u1,v1 implies u,v // (u#u1),(v#v1)
 proof assume A1: u,v // u1,v1;
    now assume u<>v & u1<>v1; then consider a,b such that
  A2: 0<a & 0<b & a*(v-u) = b*(v1-u1) by A1,ANALOAF:def 1; set p=u#u1,q=v#v1;
  A3: 0<a+b by A2,ANALOAF:2;
  A4: 0<b*2 by A2,SQUARE_1:21;
    (b*2)*(q-p) = b*(2*(q-p)) by RLVECT_1:def 9
 .= b*((1+1)*q - 2*p) by RLVECT_1:48
 .= b*((1*q+1*q) - 2*p) by RLVECT_1:def 9
   .= b*((q+1*q) - 2*p) by RLVECT_1:def 9 .= b*((q+q) - 2*p) by RLVECT_1:def 9
   .= b*((v+v1) - 2*p) by Def2
   .= b*(v+(v1 - (1+1)*p)) by RLVECT_1:42
   .= b*(v+(v1 - (1*p+1*p))) by RLVECT_1:def 9
   .= b*(v+(v1 - (p+1*p))) by RLVECT_1:def 9
   .= b*(v+(v1 - (p+p))) by RLVECT_1:def 9 .= b*(v+(v1 - (u+u1))) by Def2
   .= b*(v+((v1 - u1)-u)) by RLVECT_1:41
   .= b*((v+(v1 - u1))-u) by RLVECT_1:42
   .= b*((v1 - u1)+(v-u)) by RLVECT_1:42 .= a*(v - u)+b*(v-u) by A2,RLVECT_1:
def 9 .= (a+b)*(v-u) by RLVECT_1:def 9;
 hence thesis by A3,A4,ANALOAF:def 1
; end; hence thesis by Th10,ANALOAF:18; end;

Lm2: u,v // u1,v1 implies u,v '||' (u#v1),(v#u1)
 proof assume A1: u,v // u1,v1;
 A2: now assume u=v; then u,v // (u#v1),(v#u1) by ANALOAF:18;
  hence thesis by Def1; end;
 A3: now assume u1=v1; then u,v // (u#v1),(v#u1) by Th10;
  hence thesis by Def1; end;
    now assume u<>v & u1<>v1; then consider a,b such that
  A4: 0<a & 0<b & a*(v-u) = b*(v1-u1) by A1,ANALOAF:def 1;
  set p=u#v1,q=v#u1, A=b*2,D=b-a;
  A5: A*(q-p) = D*(v-u) proof
   A6: b*(u1-v1) = b*(-(v1-u1)) by VECTSP_1:81 .= -(a*(v-u)) by A4,RLVECT_1:39
 .= a*(-(v-u)) by RLVECT_1:39
   .= (-a)*(v-u) by RLVECT_1:38;
   thus A*(q-p) = b*(2*(q-p)) by RLVECT_1:def 9 .= b*((1+1)*q - 2*p) by
RLVECT_1:48 .= b*((1*q+1*q) - 2*p) by RLVECT_1:def 9
   .= b*((q+1*q) - 2*p) by RLVECT_1:def 9 .= b*((q+q) - 2*p) by RLVECT_1:def 9
   .= b*((v+u1) - 2*p) by Def2
   .= b*(v+(u1 - (1+1)*p)) by RLVECT_1:42
   .= b*(v+(u1 - (1*p+1*p))) by RLVECT_1:def 9 .= b*(v+(u1 - (p+1*p)))
   by RLVECT_1:def 9 .= b*(v+(u1 - (p+p))) by RLVECT_1:def 9
   .= b*(v+(u1 - (u+v1))) by Def2
   .= b*(v+((u1 - v1)-u)) by RLVECT_1:41 .= b*((v+(u1 - v1))-u) by RLVECT_1:42
   .= b*((u1 - v1)+(v-u)) by RLVECT_1:42
   .= (-a)*(v-u)+b*(v-u) by A6,RLVECT_1:def 9
   .= (b+(-a))*(v-u) by RLVECT_1:def 9
   .= D*(v-u) by XCMPLX_0:def 8; end;
     A<>0 by A4,SQUARE_1:21;
  then u,v // p,q or u,v // q,p by A5,ANALMETR:18;
  hence thesis by Def1; end; hence thesis by A2,A3; end;

Lm3: u1#u2 = v1#v2 implies v1-u1 = -(v2-u2)
proof assume A1: u1#u2=v1#v2; set p=u1#u2;
A2:p+p = u1+u2 & p+p = v1+v2 by A1,Def2;
   (v1-u1)+v2 = (v2+v1)-u1 by RLVECT_1:42
.= u2 by A2,RLSUB_2:78;
 then (v1-u1)+(v2-u2) = u2-u2 by RLVECT_1:42
 .= 0.V by RLVECT_1:28; hence thesis by RLVECT_1:19; end;

Lm4: Gen w,y & u,v,u1,v1 are_Ort_wrt w,y implies
 (u1,v1,u,v are_Ort_wrt w,y & u,v,v1,u1 are_Ort_wrt w,y)
proof assume that Gen w,y and A1: u,v,u1,v1 are_Ort_wrt w,y;
A2: v-u,v1-u1 are_Ort_wrt w,y by A1,ANALMETR:def 3;
then v1-u1,v-u are_Ort_wrt w,y by ANALMETR:8; hence u1,v1,u,v are_Ort_wrt w,y
by ANALMETR:def 3; A3: v-u,(-1)*(v1-u1) are_Ort_wrt w,y by A2,ANALMETR:11;
  (-1)*(v1-u1) = -(v1-u1) by RLVECT_1:29 .= (-v1)+u1 by RLVECT_1:47
 .= u1-v1 by RLVECT_1:def 11;
hence u,v,v1,u1 are_Ort_wrt w,y by A3,ANALMETR:def 3; end;

Lm5: Gen w,y implies u,v,u1,u1 are_Ort_wrt w,y
 proof assume A1: Gen w,y; u1-u1 = 0.V by RLVECT_1:28;
 then v-u,u1-u1 are_Ort_wrt w,y by A1,ANALMETR:9; hence thesis by ANALMETR:def
3
; end;

Lm6: Gen w,y & u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y implies
 u,v,v1,v2 are_Ort_wrt w,y proof assume that A1: Gen w,y and
 A2: u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y;
   v-u,v1-w1 are_Ort_wrt w,y & v-u,v2-w1 are_Ort_wrt w,y by A2,ANALMETR:def 3;
 then A3: v-u,(v2-w1)-(v1-w1) are_Ort_wrt w,y by A1,ANALMETR:14;
   (v2-w1)-(v1-w1) = v2-(w1+(v1-w1)) by RLVECT_1:41
 .= v2-(v1-(w1-w1)) by RLVECT_1:43 .= v2-(v1-0.V) by RLVECT_1:28
  .= v2-v1 by RLVECT_1:26; hence
   thesis by A3,ANALMETR:def 3; end;

Lm7: Gen w,y & u,v,u,v are_Ort_wrt w,y implies u=v proof assume that
 A1: Gen w,y and A2: u,v,u,v are_Ort_wrt w,y; v-u,v-u are_Ort_wrt w,y by A2,
ANALMETR:def 3; then v-u = 0.V by A1,ANALMETR:15;
 hence u=v by RLVECT_1:35; end;

Lm8: Gen w,y implies u,v,u1,u1 are_Ort_wrt w,y & u1,u1,u,v are_Ort_wrt w,y
proof assume A1: Gen w,y; u1-u1 = 0.V by RLVECT_1:28;
 then v-u,u1-u1 are_Ort_wrt w,y by A1,ANALMETR:9;
 hence u,v,u1,u1 are_Ort_wrt w,y by ANALMETR:def 3; hence
   u1,u1,u,v are_Ort_wrt w,y by A1,Lm4; end;

Lm9: Gen w,y & (u1,v1 '||' u,v or u,v '||' u1,v1) &
  (u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y) & u<>v
  implies u1,v1,u2,v2 are_Ort_wrt w,y & u2,v2,u1,v1 are_Ort_wrt w,y
proof assume that A1: Gen w,y and A2: u1,v1 '||' u,v or u,v '||' u1,v1 and
 A3: u2,v2,u,v are_Ort_wrt w,y or u,v,u2,v2 are_Ort_wrt w,y and A4: u<>v;
 reconsider S=AMSpace(V,w,y) as OrtAfSp by A1,ANALMETR:44;
 reconsider p'=u,q'=v,p1'=u1,q1'=v1,p2'=u2,q2'=v2 as Element of the
 carrier of AMSpace(V,w,y) by ANALMETR:28
; reconsider p=p',q=q',p1=p1',q1=q1',p2=p2',q2=q2'
 as Element of S;
 A5: p2,q2 _|_ p,q or p,q _|_ p2,q2 by A3,ANALMETR:31; p1,q1 // p,q or
 p,q // p1,q1 by A2,Th4; then p1,q1 _|_ p2,q2 & p2,q2 _|_ p1,q1
 by A4,A5,ANALMETR:84; hence thesis by ANALMETR:31; end;

definition let V; let w,y,u,u1,v,v1;
  pred u,u1,v,v1 are_DTr_wrt w,y means :Def3:
  u,u1 // v,v1 & u,u1,u#u1,v#v1 are_Ort_wrt w,y &
   v,v1,u#u1,v#v1 are_Ort_wrt w,y;
end;

theorem Gen w,y implies u,u,v,v are_DTr_wrt w,y
 proof assume A1: Gen w,y; A2: u,u // v,v by ANALOAF:18;
   u#u,v#v,u,u are_Ort_wrt w,y & u#u,v#v,v,v are_Ort_wrt w,y by A1,Lm5;
  then u,u,u#u,v#v are_Ort_wrt w,y & v,v,u#u,v#v are_Ort_wrt w,y by A1,Lm4;
 hence thesis by A2,Def3; end;

theorem Gen w,y implies u,v,u,v are_DTr_wrt w,y
 proof assume A1: Gen w,y; A2: u,v // u,v by ANALOAF:17;
   u,v,u#v,u#v are_Ort_wrt w,y by A1,Lm5; hence thesis by A2,Def3; end;

theorem Th19: u,v,v,u are_DTr_wrt w,y implies u=v
 proof assume u,v,v,u are_DTr_wrt w,y; then u,v // v,u by Def3;
 hence thesis by ANALOAF:19; end;

theorem Th20: Gen w,y & v1,u,u,v2 are_DTr_wrt w,y implies v1=u & u=v2
proof assume that A1: Gen w,y and A2: v1,u,u,v2 are_DTr_wrt w,y;
 set a=v1#u, b=u#v2; A3: v1,u // u,v2 & v1,u,a,b are_Ort_wrt w,y &
 u,v2,a,b are_Ort_wrt w,y by A2,Def3;
    v1<>v2 implies thesis proof assume v1<>v2;
   then A4: a<>b by Th9;
     a,u // u,b by A3,Th15; then a,u // a,b & u,b // a,b by Lm1;
   then A5: a,u '||' a,b & u,b '||' a,b by Def1; u,v2 // u,b & v1,u // a,u by
Th14
; then A6: v1,u '||' a,u & u,v2 '||' u,b by Def1;
   A7: v1=u proof assume A8: v1<>u;
    A9: u<>a proof assume u=a; then v1#u=u#u;
     hence contradiction by A8,Th9; end;
      a,u,a,b are_Ort_wrt w,y by A1,A3,A6,A8,Lm9; then a,u,a,u are_Ort_wrt w,y
    by A1,A4,A5,Lm9; hence contradiction by A1,A9,Lm7; end;
      u=v2 proof assume A10: u<>v2;
    A11: u<>b proof assume u=b; then u#v2=u#u;
    hence contradiction by A10,Th9; end;
      u,b,a,b are_Ort_wrt w,y by A1,A3,A6,A10,Lm9; then u,b,u,b are_Ort_wrt w,
y
    by A1,A4,A5,Lm9; hence contradiction by A1,A11,Lm7; end;
   hence thesis by A7; end;
 hence thesis by A2,Th19; end;

theorem Th21: Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y
  & u<>v implies u1,v1,u2,v2 are_DTr_wrt w,y
 proof assume that A1: Gen w,y and A2: u,v,u1,v1 are_DTr_wrt w,y &
  u,v,u2,v2 are_DTr_wrt w,y and A3: u<>v;
  A4: u,v // u1,v1 & u,v,u#v,u1#v1 are_Ort_wrt w,y &
  u1,v1,u#v,u1#v1 are_Ort_wrt w,y by A2,Def3;
  A5: u,v // u2,v2 & u,v,u#v,u2#v2 are_Ort_wrt w,y &
  u2,v2,u#v,u2#v2 are_Ort_wrt w,y by A2,Def3;
  then A6: u,v '||' u2,v2 & u,v '||' u1,v1 by A4,Def1;
  A7: u1,v1 // u2,v2 by A3,A4,A5,ANALOAF:20;
  set a=u1#v1, b=u2#v2; u,v,a,b are_Ort_wrt w,y by A1,A4,A5,Lm6;
  then u1,v1,a,b are_Ort_wrt w,y & u2,v2,a,b are_Ort_wrt w,y by A1,A3,A6,Lm9;
 hence thesis by A7,Def3; end;

theorem Th22: Gen w,y implies ex t being VECTOR of V st
 (u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y)
 proof assume A1: Gen w,y; set a=u#v;
 A2: now assume A3: u=v; u,u // u1,u1 & u#u,u1#u1,u,u are_Ort_wrt w,y &
  u#u,u1#u1,u1,u1 are_Ort_wrt w,y by A1,Lm5,ANALOAF:18; then u,u // u1,u1 &
  u,u,u#u,u1#u1 are_Ort_wrt w,y & u1,u1,u#u,u1#u1 are_Ort_wrt w,y by A1,Lm4;
  then u,u,u1,u1 are_DTr_wrt w,y by Def3; hence thesis by A3; end;
    now assume A4: u<>v;
     a<>u proof assume a=u; then u#u = u#v;
hence contradiction by A4,Th9; end;
  then u-a<>0.V by RLVECT_1:35;
  then consider r being Real such that A5: (u1-a)-r*(u-a),u-a are_Ort_wrt w,y
  by A1,ANALMETR:17; set b = u1-r*(u-a); set t = 2*b-u1;
  A6: u-v = 2*(u-u#v) by Th12;
  A7: u1#t = b proof u1+t
   = (1+1)*b by RLSUB_2:78 .= 1*b+1*b by RLVECT_1:def 9 .= b+1*b by RLVECT_1:
def 9 .= b+b by RLVECT_1:def 9; hence thesis by Def2; end;
A8:   u1-(a+r*(u-a)) = (u1-r*(u-a))-a by RLVECT_1:41;
then A9:   b-a = (u1-a)-r*(u-a) by RLVECT_1:41;
  A10: b-a,u-a are_Ort_wrt w,y by A5,A8,RLVECT_1:41; b-a,u-v are_Ort_wrt w,y
by A5,A6,A9,ANALMETR:11; then a,b,v,u are_Ort_wrt w,y by ANALMETR:def 3;
   then a,b,u,v are_Ort_wrt w,y by A1,Lm4;
   then A11: u,v,u#v,u1#t are_Ort_wrt w,y by A1,A7,Lm4;
    u1-b = (u1-u1)+r*(u-a) by RLVECT_1:43
   .= 0.V + r*(u-a) by RLVECT_1:28 .= r*(u-a) by RLVECT_1:10;
  then A12: u1-t = 2*(r*(u-a)) by A7,Th12 .= (2*r)*(u-a) by RLVECT_1:def 9;
  then A13: u1-t = r*(u-v) by A6,RLVECT_1:def 9;
  A14: now assume A15: r=0; A16: b=u1 & t=u1
    proof thus b = u1-0.V by A15,RLVECT_1:23 .= u1 by RLVECT_1:26
; hence t = (1+1)*u1-u1 .= (1*u1+1*u1)-u1 by RLVECT_1:def 9 .= (u1+1*u1)-u1
by RLVECT_1:def 9 .= (u1+u1)-u1 by RLVECT_1:def 9
    .= u1 by RLSUB_2:78; end;
      u,v // u1,t & u1,t,u#v,u1#t are_Ort_wrt w,y proof thus u,v // u1,t by A16
,ANALOAF:18; a,b,u1,t are_Ort_wrt w,y by A1,A16,Lm5;
    hence thesis by A1,A7,Lm4
; end; then u,v,u1,t are_DTr_wrt w,y by A11,Def3;
   hence thesis; end;
     now assume r<>0; b-a,u1-t are_Ort_wrt w,y by A10,A12,ANALMETR:11;
    then A17: a,b,t,u1 are_Ort_wrt w,y by ANALMETR:def 3
; then a,b,u1,t are_Ort_wrt w,y
    by A1,Lm4;
    then A18: u1,t,u#v,u1#t are_Ort_wrt w,y by A1,A7,Lm4;
    A19: t,u1,u#v,t#u1 are_Ort_wrt w,y by A1,A7,A17,Lm4;
      r*(u-v) = 1*(u1-t) by A13,RLVECT_1:def 9;
    then v,u // t,u1 or v,u // u1,t by ANALMETR:18;
    then u,v // u1,t or u,v // t,u1 by ANALOAF:21; hence u,v,u1,t are_DTr_wrt
w,y
    or u,v,t,u1 are_DTr_wrt w,y by A11,A18,A19,Def3; end;
  hence thesis by A14; end; hence thesis by A2; end;

theorem Th23: Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies
 u1,v1,u,v are_DTr_wrt w,y
  proof assume that A1: Gen w,y and A2: u,v,u1,v1 are_DTr_wrt w,y;
    u,v // u1,v1 & u,v,u#v,u1#v1 are_Ort_wrt w,y &
   u1,v1,u#v,u1#v1 are_Ort_wrt w,y by A2,Def3;
  then u1,v1 // u,v & u1,v1,u1#v1,u#v are_Ort_wrt w,y &
   u,v,u1#v1,u#v are_Ort_wrt w,y by A1,Lm4,ANALOAF:21;
  hence thesis by Def3; end;

theorem Th24: Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies
 v,u,v1,u1 are_DTr_wrt w,y
  proof assume that A1: Gen w,y and A2: u,v,u1,v1 are_DTr_wrt w,y;
  A3: u,v // u1,v1 & u,v,u#v,u1#v1 are_Ort_wrt w,y &
   u1,v1,u#v,u1#v1 are_Ort_wrt w,y by A2,Def3;
   now let u,u',v,v' be VECTOR of V; assume u,u',v,v' are_Ort_wrt w,y;
   then v,v',u,u' are_Ort_wrt w,y by A1,Lm4; then v,v',u',u are_Ort_wrt w,y
by A1,Lm4; hence u',u,v,v' are_Ort_wrt w,y by A1,Lm4; end;
  then v,u // v1,u1 &
  v,u,v#u,v1#u1 are_Ort_wrt w,y & v1,u1,v#u,v1#u1 are_Ort_wrt w,y
  by A3,ANALOAF:21; hence thesis by Def3; end;

Lm10: Gen w,y & u<>v & u,v '||' u,u1 & u,v '||' u,v1 &
u,v '||' u,u2 & u,v '||' u,v2
  implies u1,v1 '||' u2,v2
proof assume that A1: Gen w,y and A2: u<>v and
 A3: u,v '||' u,u1 & u,v '||' u,v1 & u,v '||' u,u2 & u,v '||' u,v2;
reconsider p'=u,q'=v,p1'=u1,q1'=v1,p2'=u2,q2'=v2 as
 Element of Lambda(OASpace(V)) by ANALMETR:22;
 reconsider S' = OASpace(V) as OAffinSpace by A1,Th1; reconsider
 S = Lambda(S') as AffinSpace by DIRAF:48;
 reconsider p=p',q=q',p1=p1',q1=q1',p2=p2',q2=q2' as Element of the
 carrier of S; p,q // p,p1 & p,q // p,q1 & p,q // p,p2 & p,q // p,
 q2 by A1,A3,Th3;
 then LIN p,q,p1 & LIN p,q,q1 & LIN p,q,p2 & LIN p,q,q2 by AFF_1:def 1;
 then LIN p1,q1,p2 & LIN p1,q1,q2 by A2,AFF_1:17; then p1,q1 // p2,q2 by AFF_1:
19;
 hence thesis by A1,Th3; end;

theorem Th25: Gen w,y & v,u1,v,u2 are_DTr_wrt w,y implies u1=u2
proof assume that A1: Gen w,y and A2: v,u1,v,u2 are_DTr_wrt w,y;
 A3: v,u1 // v,u2 & v,u1,v#u1,v#u2 are_Ort_wrt w,y &
 v,u2,v#u1,v#u2 are_Ort_wrt w,y by A2,Def3;
 set b=v#u1, c = v#u2; assume A4: u1<>u2;
 then A5: b<>c by Th9;
 A6: v,u1 // v,u2 & v,u2 // v,u1 by A3,ANALOAF:21;
 A7: v,u1 // v,b & v,u2 // v,c by Th14;
 A8: v,u1 // v,u1 & v,u1 // v,v & v,u2 // v,u2 & v,u2 // v,v
    by ANALOAF:17,18;
 A9: v,u1 // v,c proof
      now assume v<>c; then v<>u2;
    hence thesis by A6,A7,ANALOAF:20; end;
   hence thesis by ANALOAF:18; end;
 A10: v,u2 // v,b proof
      now assume v<>b; then v<>u1;
    hence thesis by A3,A7,ANALOAF:20; end;
   hence thesis by ANALOAF:18; end;
 A11: v,u1 '||' v,b & v,u2 '||' v,c by A7,Def1;
 A12: v,u1 '||' v,u1 & v,u1 '||' v,v & v,u2 '||' v,u2 &
                            v,u2 '||' v,v by A8,Def1;
 A13: v,u1 '||' v,c by A9,Def1; A14: v,u2 '||' v,b by A10,Def1;
 A15: now assume A16: v<>u1; then v,u1 '||' b,c by A1,A11,A12,A13,Lm10;
  then b,c,b,c are_Ort_wrt w,y by A1,A3,A16,Lm9;
  hence contradiction by A1,A5,Lm7; end;
    now assume A17: v<>u2; then v,u2 '||' b,c by A1,A11,A12,A14,Lm10;
  then b,c,b,c are_Ort_wrt w,y by A1,A3,A17,Lm9;
  hence contradiction by A1,A5,Lm7; end;
hence thesis by A4,A15; end;

theorem Th26: Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y
 implies (u=v or v1=v2)
proof assume that A1: Gen w,y and A2: u,v,u1,v1 are_DTr_wrt w,y &
 u,v,u1,v2 are_DTr_wrt w,y; assume u<>v; then u1,v1,u1,v2 are_DTr_wrt w,y
 by A1,A2,Th21; hence v1=v2 by A1,Th25; end;

theorem Th27: (Gen w,y & u<>u1 & u,u1,v,v1 are_DTr_wrt w,y &
 (u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y)) implies v1=v2
proof assume that A1: Gen w,y & u<>u1 & u,u1,v,v1 are_DTr_wrt w,y and
 A2: u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y;
   now assume u,u1,v2,v are_DTr_wrt w,y; then v2,v,v,v1 are_DTr_wrt w,y
 by A1,Th21; then v=v2 & v=v1 by A1,Th20; hence thesis; end;
hence thesis by A1,A2,Th26; end;

theorem Th28: Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies
      u,v,(u#u1),(v#v1) are_DTr_wrt w,y
proof assume that A1: Gen w,y and A2: u,v,u1,v1 are_DTr_wrt w,y;
set p=u#u1,q=v#v1,r=u#v,s=u1#v1;
A3: u,v // u1,v1 & u,v,r,s are_Ort_wrt w,y & u1,v1,r,s are_Ort_wrt w,y
 by A2,Def3; p#q = r#s by Th8; then r,s // r,p#q by Th14;
 then A4: r,s '||' r,p#q by Def1;
 A5: u,v // (u#u1),(v#v1) by A3,Th16; then A6: u,v '||' p,q by Def1;
   u1,v1 // u,v by A3,ANALOAF:21;
 then u1,v1 // (u1#u),(v1#v) & u#u1=u1#u & v#v1=v1#v by Th16;
then A7: u1,v1 '||' p,q by Def1;
 A8: now assume r=s; then r=r#s .= p#q by Th8;
 hence u1,v1,r,(p#q) are_Ort_wrt w,y &
  u,v,r,(p#q) are_Ort_wrt w,y by A1,Lm8; end;
 A9:  r<>s implies u1,v1,r,(p#q) are_Ort_wrt w,y &
  u,v,r,(p#q) are_Ort_wrt w,y by A1,A3,A4,Lm9;
 then A10:  u<>v implies p,q,r,(p#q) are_Ort_wrt w,y by A1,A6,A8,Lm9;
A11:  u=v & u1<>v1 implies p,q,r,(p#q) are_Ort_wrt w,y by A1,A7,A8,A9,Lm9;
     u=v & u1=v1 implies p,q,r,(p#q) are_Ort_wrt w,y by A1,Lm8;
hence thesis by A5,A8,A9,A10,A11,Def3; end;

theorem Th29: Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies
 (u,v,(u#v1),(v#u1) are_DTr_wrt w,y or u,v,(v#u1),(u#v1) are_DTr_wrt w,y)
proof assume that A1: Gen w,y and A2: u,v,u1,v1 are_DTr_wrt w,y;
set p=u#v1,q=v#u1,r=u#v,s=u1#v1;
A3: u,v // u1,v1 & u,v,r,s are_Ort_wrt w,y & u1,v1,r,s are_Ort_wrt w,y
 by A2,Def3; A4: p#q = r#s by Th8;
 then r,s // r,p#q by Th14; then A5: r,s '||' r,p#q by Def1;
A6: u,v '||' p,q by A3,Lm2;
then A7: u,v // p,q or u,v // q,p by Def1;
   now assume A8: u<>v & u1<>v1;
 A9: now assume A10:r=s;
 then A11: u,v,r,(p#q) are_Ort_wrt w,y & u,v,r,(q#p) are_Ort_wrt w,y
 by A1,A4,Lm8;
    p,q,r,(p#q) are_Ort_wrt w,y & q,p,r,(q#p) are_Ort_wrt w,y
   by A1,A4,A10,Lm8; hence u,v,p,q are_DTr_wrt w,y or u,v,q,p are_DTr_wrt w,y
 by A7,A11,Def3; end;
    now assume r<>s;
then A12: u,v,r,(p#q) are_Ort_wrt w,y by A1,A3,A5,Lm9;
     then r,(p#q),p,q are_Ort_wrt w,y by A1,A6,A8,Lm9;
     then r,(p#q),q,p are_Ort_wrt w,y by A1,Lm4;
  then p,q,r,(p#q) are_Ort_wrt w,y & q,p,r,(q#p) are_Ort_wrt w,y
   by A1,A6,A8,A12,Lm4,Lm9
; hence u,v,p,q are_DTr_wrt w,y or u,v,q,p are_DTr_wrt w,y
 by A7,A12,Def3; end;
 hence thesis by A9; end; hence thesis by A1,A2,Th28; end;

theorem Th30: for u,u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of V holds
 (Gen w,y & u=u1#t1 & u=u2#t2 & u=v1#w1 & u=v2#w2 &
  u1,u2,v1,v2 are_DTr_wrt w,y implies t1,t2,w1,w2 are_DTr_wrt w,y)
proof let u,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V; assume that A1: Gen w,y
and A2: u=u1#t1 & u=u2#t2 & u=v1#w1 & u=v2#w2 and
A3: u1,u2,v1,v2 are_DTr_wrt w,y; set p=u1#u2,q=v1#v2,r=t1#t2,s=w1#w2;
A4: u1,u2 // v1,v2 & u1,u2,p,q are_Ort_wrt w,y & v1,v2,p,q are_Ort_wrt w,y
 by A3,Def3;
A5: u2-u1 = -(t2-t1) & v2-v1 = -(w2-w1) by A2,Lm3;
 A6:now assume u1=u2; then t1=t2 by A2,Th9; hence t1,t2 // w1,w2 &
 t1,t2,r,s are_Ort_wrt w,y by A1,Lm8,ANALOAF:18; end;
 A7:now assume v1=v2; then w1=w2 by A2,Th9; hence t1,t2 // w1,w2 &
 w1,w2,r,s are_Ort_wrt w,y by A1,Lm8,ANALOAF:18; end;
A8: t1,t2 // w1,w2 proof
    now assume u1<>u2 & v1<>v2; then consider a,b such that A9: 0<a & 0<b &
  a*(u2-u1)=b*(v2-v1) by A4,ANALOAF:def 1;
   a*(t2-t1) = a*(-(-(t2-t1))) by RLVECT_1:30 .= -(b*(-(w2-w1))) by A5,A9,
RLVECT_1:39 .= b*(-(-(w2-w1))) by RLVECT_1:39
  .= b*(w2-w1) by RLVECT_1:30;
  hence thesis by A9,ANALOAF:def 1; end; hence thesis by A6,A7; end;
  u=p#r & u=q#s proof thus p#r = u#u by A2,Th8 .=u;
 thus q#s = u#u by A2,Th8
  .=u; end;
 then A10: s-r = -(q-p) by Lm3
 .= (-1)*(q-p) by RLVECT_1:29;
   t2-t1 = -(u2-u1) & w2-w1 = -(v2-v1) by A2,Lm3;
 then A11: t2-t1 = (-1)*(u2-u1) & w2-w1 = (-1)*(v2-v1) by RLVECT_1:29;
   u2-u1,q-p are_Ort_wrt w,y & v2-v1,q-p are_Ort_wrt w,y by A4,ANALMETR:def 3;
 then t2-t1,s-r are_Ort_wrt w,y & w2-w1,s-r are_Ort_wrt w,y
 by A10,A11,ANALMETR:10; then t1,t2,r,s are_Ort_wrt w,y &
 w1,w2,r,s are_Ort_wrt w,y by ANALMETR:def 3
; hence thesis by A8,Def3; end;

Lm11: v1 = b1*w + b2*y & v2 = c1*w + c2*y implies
 v1 + v2 = (b1 + c1)*w + (b2 + c2)*y & v1 - v2 = (b1 - c1)*w + (b2 - c2)*y
 proof assume that A1: v1 = b1*w + b2*y and A2: v2 = c1*w + c2*y;
 thus v1 + v2 = ((b1*w + b2*y) + c1*w) + c2*y by A1,A2,RLVECT_1:def 6
  .= ((b1*w + c1*w) + b2*y) + c2*y by RLVECT_1:def 6
  .= ((b1 + c1)*w + b2*y) + c2*y by RLVECT_1:def 9
  .= (b1 + c1)*w + (b2*y + c2*y) by RLVECT_1:def 6
  .= (b1 + c1)*w + (b2 + c2)*y by RLVECT_1:def 9;
 thus v1 - v2 = (b1*w + b2*y)+(-(c1*w + c2*y)) by A1,A2,RLVECT_1:def 11
  .= (b1*w + b2*y)+(-(c1*w) + -(c2*y)) by RLVECT_1:45
  .= (b1*w + b2*y)+(c1*(-w) + -(c2*y)) by RLVECT_1:39
  .= (b1*w + b2*y)+(c1*(-w) + c2*(-y)) by RLVECT_1:39
  .= (b1*w + b2*y)+((-c1)*w + c2*(-y)) by RLVECT_1:38
  .= (b1*w + b2*y)+((-c1)*w + (-c2)*y) by RLVECT_1:38
  .= ((b1*w + b2*y) + (-c1)*w) + (-c2)*y by RLVECT_1:def 6
  .= ((b1*w + (-c1)*w) + b2*y) + (-c2)*y by RLVECT_1:def 6
  .= ((b1 + (-c1))*w + b2*y) + (-c2)*y by RLVECT_1:def 9
  .= (b1 + (-c1))*w + (b2*y + (-c2)*y) by RLVECT_1:def 6
  .= (b1 + (-c1))*w + (b2 + (-c2))*y by RLVECT_1:def 9
  .= (b1 - c1)*w + (b2 + (-c2))*y by XCMPLX_0:def 8
  .= (b1 - c1)*w + (b2 - c2)*y by XCMPLX_0:def 8; end;

Lm12: v = b1*w + b2*y implies a*v = (a*b1)*w + (a*b2)*y proof
  assume v= b1*w + b2*y; hence a*v = a*(b1*w) + a*(b2*y)
    by RLVECT_1:def 9 .= (a*b1)*w + a*(b2*y) by RLVECT_1:def 9
    .= (a*b1)*w + (a*b2)*y by RLVECT_1:def 9; end;

Lm13: Gen w,y & a1*w + a2*y = b1*w + b2*y implies a1=b1 & a2=b2 proof
 assume that A1: Gen w,y and A2: a1*w+a2*y=b1*w+b2*y;
   0.V = (a1*w+a2*y)-(b1*w+b2*y) by A2,RLVECT_1:28 .= (a1-b1)*w+(a2-b2)*y by
Lm11
;
 then a1-b1=0 & a2-b2=0 by A1,ANALMETR:def 1
; then -b1 + a1 =0 & -b2 + a2 = 0 by XCMPLX_0:def 8;
 then a1=-(-b1) & a2=-(-b2) by XCMPLX_0:def 6; hence thesis; end;

definition let V,w,y,u such that A1: Gen w,y;
  func pr1(w,y,u) -> Real means
 :Def4: ex b st u=it*w+b*y;
 existence by A1,ANALMETR:def 1;
 uniqueness by A1,Lm13; end;

definition let V,w,y,u such that A1: Gen w,y;
  func pr2(w,y,u) -> Real means
 :Def5: ex a st u=a*w+it*y;
 existence proof consider a,b such that A2: u = a*w+b*y by A1,ANALMETR:def 1;
 take b; thus thesis by A2; end;
 uniqueness by A1,Lm13; end;

Lm14: Gen w,y implies u = pr1(w,y,u)*w + pr2(w,y,u)*y
 proof assume A1: Gen w,y;
  then ex b st u = (pr1(w,y,u))*w + b*y by Def4;
 hence thesis by A1,Def5; end;

Lm15: (Gen w,y & u=a*w+b*y) implies a=pr1(w,y,u) & b=pr2(w,y,u)
 proof assume A1: Gen w,y & u=a*w+b*y;
  then u = pr1(w,y,u)*w + pr2(w,y,u)*y by Lm14; hence thesis by A1,Lm13; end;

Lm16: Gen w,y implies ( pr1(w,y,u+v) = pr1(w,y,u)+pr1(w,y,v) &
   pr2(w,y,u+v) = pr2(w,y,u)+pr2(w,y,v) &
   pr1(w,y,u-v) = pr1(w,y,u)-pr1(w,y,v) &
   pr2(w,y,u-v) = pr2(w,y,u)-pr2(w,y,v) & pr1(w,y,a*u) = a*pr1(w,y,u) &
   pr2(w,y,a*u) = a*pr2(w,y,u))
 proof assume A1: Gen w,y; set p1u = pr1(w,y,u), p2u = pr2(w,y,u),
  p1v = pr1(w,y,v), p2v = pr2(w,y,v);
  A2: u = p1u*w + p2u*y & v = p1v*w + p2v*y by A1,Lm14;
   then u + v = (p1u*w + p2u*y + p1v*w) + p2v*y by RLVECT_1:def 6
   .= ((p1u*w + p1v*w) + p2u*y) + p2v*y by RLVECT_1:def 6
   .= (p1u*w + p1v*w) + (p2u*y + p2v*y) by RLVECT_1:def 6
   .= (p1u + p1v)*w + (p2u*y + p2v*y) by RLVECT_1:def 9
   .= (p1u + p1v)*w + (p2u + p2v)*y by RLVECT_1:def 9;
   hence pr1(w,y,u+v) = p1u + p1v & pr2(w,y,u+v) = p2u + p2v by A1,Lm15;
     u - v = (p1u - p1v)*w + (p2u - p2v)*y by A2,Lm11;
   hence pr1(w,y,u-v) = p1u - p1v & pr2(w,y,u-v) = p2u - p2v by A1,Lm15;
     a*u = (a*p1u)*w + (a*p2u)*y by A2,Lm12;
 hence pr1(w,y,a*u) = a*pr1(w,y,u) & pr2(w,y,a*u) = a*pr2(w,y,u) by A1,Lm15;
 end;

Lm17: Gen w,y implies (2*pr1(w,y,u#v) = pr1(w,y,u)+pr1(w,y,v) &
    2*pr2(w,y,u#v) = pr2(w,y,u)+pr2(w,y,v))
 proof assume A1: Gen w,y; set p=u#v;
    2*(u#v) = (1+1)*p .= 1*p + 1*p by RLVECT_1:def 9
  .= p + 1*p by RLVECT_1:def 9 .= p+p by RLVECT_1:def 9 .= u+v by Def2;
  then 2*pr1(w,y,u#v) = pr1(w,y,u+v) & 2*pr2(w,y,u#v) = pr2(w,y,u+v)
  by A1,Lm16;
  hence thesis by A1,Lm16; end;

Lm18: a*(b+c)+a1*(b1+c1) = (a*b+a1*b1)+(a*c+a1*c1)
 proof thus a*(b+c)+a1*(b1+c1) = (a*b+a*c)+a1*(b1+c1) by XCMPLX_1:8 .=
(a*b+a*c)+(a1*b1+a1*c1) by XCMPLX_1:8 .= ((a*b+a*c)+a1*b1)+a1*c1 by XCMPLX_1:1
 .=
((a*b+a1*b1)+a*c)+a1*c1 by XCMPLX_1:1 .= (a*b+a1*b1)+(a*c+a1*c1) by XCMPLX_1:1;
 end;

Lm19: -u + -v = -(u+v)
proof (u+v)+(-u + -v) = ((u+v)+ -u) + -v by RLVECT_1:def 6 .=
 (v+(u+ -u)) + -v by RLVECT_1:def 6 .=
 (v+0.V) + -v by RLVECT_1:16 .= v + -v by RLVECT_1:10 .= 0.V by RLVECT_1:16;
hence thesis by RLVECT_1:def 10; end;

Lm20: a*(b-c)+a1*(b1-c1) = (a*b+a1*b1)-(a*c+a1*c1)
proof thus a*(b-c)+a1*(b1-c1) = a*(b+ -c)+a1*(b1-c1) by XCMPLX_0:def 8 .=
  a*(b+ -c)+a1*(b1+ -c1) by XCMPLX_0:def 8 .= (a*b+a1*b1)+(a*(-c)+a1*(-c1))
  by Lm18 .= (a*b+a1*b1)+(-a*c + a1*(-c1)) by XCMPLX_1:175
  .= (a*b+a1*b1)+(-a*c + -a1*c1) by XCMPLX_1:175
 .= (a*b+a1*b1)+ -(a*c+a1*c1)
  by XCMPLX_1:140 .= (a*b+a1*b1)-(a*c+a1*c1) by XCMPLX_0:def 8; end;

Lm21: (a*b)*c + (a*b1)*c1 = a*(b*c+b1*c1)
proof thus (a*b)*c + (a*b1)*c1 = a*(b*c) + (a*b1)*c1 by XCMPLX_1:4 .=
  a*(b*c) + a*(b1*c1) by XCMPLX_1:4 .= a*(b*c + b1*c1) by XCMPLX_1:8; end;

Lm22: ((a+(b-2*a))+a)-b = 0
 proof thus ((a+(b-2*a))+a)-b = ((1*a+1*a)+(b-2*a))-b by XCMPLX_1:1
 .= (((1+1)*a)+(b-2*a))-b by XCMPLX_1:8
  .= (b-(2*a-2*a))-b by XCMPLX_1:37 .= (b-0)-b by XCMPLX_1:14
  .=0 by XCMPLX_1:14; end;

Lm23: (u2 + a2*v) - (u1 + a1*v) = (u2-u1) + (a2-a1)*v
 proof thus (u2+a2*v) - (u1+a1*v) = ((u2+a2*v) -u1)-a1*v by RLVECT_1:41 .=
 (a2*v+(u2 -u1))-a1*v by RLVECT_1:42 .=
 (u2-u1)+(a2*v-a1*v) by RLVECT_1:42 .=
 (u2 - u1)+(a2-a1)*v by RLVECT_1:49; end;

Lm24: (a-b)-(a-c) = c-b
 proof thus (a-b)-(a-c) = ((a-b)-a) + c by XCMPLX_1:37 .=(a-(a+b)) + c by
XCMPLX_1:36 .= ((a-a)-b) + c by XCMPLX_1:36 .= c + (0-b) by XCMPLX_1:14
 .= c + -b by XCMPLX_1:150 .= c - b by XCMPLX_0:def 8; end;

definition let V,w,y,u,v;
  func PProJ(w,y,u,v) -> Real equals:Def6:
  pr1(w,y,u)*pr1(w,y,v) + pr2(w,y,u)*pr2(w,y,v); correctness;
end;

theorem Th31: for u,v holds PProJ(w,y,u,v) = PProJ(w,y,v,u)
 proof let u,v be VECTOR of V;
 set a1=pr1(w,y,u),a2=pr2(w,y,u),b1=pr1(w,y,v),b2=pr2(w,y,v);
   PProJ(w,y,u,v) = b1*a1+b2*a2 by Def6 .= PProJ(w,y,v,u) by Def6;
 hence PProJ(w,y,u,v) = PProJ(w,y,v,u); end;

theorem Th32: Gen w,y implies for u,v,v1 holds
  PProJ(w,y,u,v+v1)=PProJ(w,y,u,v)+PProJ(w,y,u,v1) &
  PProJ(w,y,u,v-v1)=PProJ(w,y,u,v)-PProJ(w,y,u,v1) &
  PProJ(w,y,v-v1,u)=PProJ(w,y,v,u)-PProJ(w,y,v1,u) &
  PProJ(w,y,v+v1,u)=PProJ(w,y,v,u)+PProJ(w,y,v1,u)
 proof assume A1: Gen w,y; let u,v,v1 be VECTOR of V;
 A2: now let u,v,v1 be VECTOR of V;
 A3: PProJ(w,y,u,v+v1) = pr1(w,y,u)*pr1(w,y,v+v1)+pr2(w,y,u)*pr2(w,y,v+v1)
 by Def6
  .= pr1(w,y,u)*(pr1(w,y,v)+pr1(w,y,v1))+pr2(w,y,u)*pr2(w,y,v+v1) by A1,Lm16
  .= pr1(w,y,u)*(pr1(w,y,v)+pr1(w,y,v1))+pr2(w,y,u)*(pr2(w,y,v)+pr2(w,y,v1))
  by A1,Lm16 .= (pr1(w,y,u)*pr1(w,y,v)+pr2(w,y,u)*pr2(w,y,v))+
  (pr1(w,y,u)*pr1(w,y,v1)+pr2(w,y,u)*pr2(w,y,v1)) by Lm18 .=
  (pr1(w,y,u)*pr1(w,y,v)+pr2(w,y,u)*pr2(w,y,v)) + PProJ(w,y,u,v1) by Def6
  .= PProJ(w,y,u,v)+PProJ(w,y,u,v1) by Def6;
    PProJ(w,y,u,v-v1) = pr1(w,y,u)*pr1(w,y,v-v1)+pr2(w,y,u)*pr2(w,y,v-v1) by
Def6
  .= pr1(w,y,u)*(pr1(w,y,v)-pr1(w,y,v1))+pr2(w,y,u)*pr2(w,y,v-v1) by A1,Lm16
  .= pr1(w,y,u)*(pr1(w,y,v)-pr1(w,y,v1))+pr2(w,y,u)*(pr2(w,y,v)-pr2(w,y,v1))
  by A1,Lm16 .= (pr1(w,y,u)*pr1(w,y,v)+pr2(w,y,u)*pr2(w,y,v))-
  (pr1(w,y,u)*pr1(w,y,v1)+pr2(w,y,u)*pr2(w,y,v1)) by Lm20 .=
  (pr1(w,y,u)*pr1(w,y,v)+pr2(w,y,u)*pr2(w,y,v)) - PProJ(w,y,u,v1) by Def6
  .= PProJ(w,y,u,v)-PProJ(w,y,u,v1) by Def6;
 hence PProJ(w,y,u,v+v1)=PProJ(w,y,u,v)+PProJ(w,y,u,v1) &
   PProJ(w,y,u,v-v1)=PProJ(w,y,u,v)-PProJ(w,y,u,v1) by A3; end;
 hence PProJ(w,y,u,v+v1) = PProJ(w,y,u,v)+PProJ(w,y,u,v1) &
   PProJ(w,y,u,v-v1) = PProJ(w,y,u,v)-PProJ(w,y,u,v1);
 thus PProJ(w,y,v-v1,u) = PProJ(w,y,u,v-v1) by Th31 .= PProJ(w,y,u,v)-PProJ
(w,y,u,v1)
  by A2 .= PProJ(w,y,v,u) - PProJ(w,y,u,v1) by Th31 .= PProJ(w,y,v,u)-PProJ
(w,y,v1,u)
  by Th31;
 thus PProJ(w,y,v+v1,u)= PProJ(w,y,u,v+v1) by Th31 .= PProJ(w,y,u,v)+PProJ
(w,y,u,v1) by A2 .= PProJ(w,y,v,u) + PProJ(w,y,u,v1) by Th31
 .= PProJ(w,y,v,u)+PProJ
(w,y,v1,u)
 by Th31; end;

theorem Th33: Gen w,y implies for u,v being VECTOR of V, a being Real holds
 PProJ(w,y,a*u,v)=a*PProJ(w,y,u,v) & PProJ(w,y,u,a*v)=a*PProJ(w,y,u,v) &
 PProJ(w,y,a*u,v)=PProJ(w,y,u,v)*a & PProJ(w,y,u,a*v)=PProJ(w,y,u,v)*a
 proof assume A1: Gen w,y; let u,v be VECTOR of V,a be Real;
 A2: now let u,v be VECTOR of V,a be Real;
   PProJ(w,y,a*u,v) = pr1(w,y,a*u)*pr1(w,y,v)+pr2(w,y,a*u)*pr2(w,y,v) by Def6
 .= (a*pr1(w,y,u))*pr1(w,y,v)+pr2(w,y,a*u)*pr2(w,y,v) by A1,Lm16
 .= (a*pr1(w,y,u))*pr1(w,y,v)+(a*pr2(w,y,u))*pr2(w,y,v) by A1,Lm16
 .= a*(pr1(w,y,u)*pr1(w,y,v)+pr2(w,y,u)*pr2(w,y,v)) by Lm21
 .= a*PProJ(w,y,u,v)
  by Def6; hence PProJ(w,y,a*u,v) = a*PProJ(w,y,u,v); end;
 hence PProJ(w,y,a*u,v) = a*PProJ(w,y,u,v);
 thus PProJ(w,y,u,a*v) = PProJ(w,y,a*v,u) by Th31 .= a*PProJ(w,y,v,u) by A2
  .= a*PProJ(w,y,u,v) by Th31;
 thus PProJ(w,y,a*u,v) = PProJ(w,y,u,v)*a by A2;
 thus PProJ(w,y,u,a*v) = PProJ(w,y,a*v,u) by Th31 .= a*PProJ(w,y,v,u) by A2
  .= PProJ(w,y,u,v)*a by Th31; end;

theorem Th34: Gen w,y implies for u,v being VECTOR of V holds
  (u,v are_Ort_wrt w,y iff PProJ(w,y,u,v)=0)
  proof assume A1: Gen w,y; let u,v be VECTOR of V;
 set a1=pr1(w,y,u),a2=pr2(w,y,u),b1=pr1(w,y,v),b2=pr2(w,y,v);
 A2: u = a1*w+a2*y & v = b1*w+b2*y by A1,Lm14;
 A3: now assume u,v are_Ort_wrt w,y; then a1*b1+a2*b2 = 0 by A1,A2,ANALMETR:5
;
  hence PProJ(w,y,u,v) = 0 by Def6; end;
    now assume PProJ(w,y,u,v) = 0; then a1*b1+a2*b2 = 0 by Def6;
  hence u,v are_Ort_wrt w,y by A2,ANALMETR:def 2; end;
 hence u,v are_Ort_wrt w,y iff PProJ(w,y,u,v)=0 by A3; end;

theorem Th35: Gen w,y implies for u,v,u1,v1 being VECTOR of V holds
 (u,v,u1,v1 are_Ort_wrt w,y iff PProJ
(w,y,v-u,v1-u1)=0) proof assume A1: Gen w,y;
let u,v,u1,v1 be VECTOR of V; u,v,u1,v1 are_Ort_wrt w,y iff
 v-u,v1-u1 are_Ort_wrt w,y by ANALMETR:def 3;
 hence u,v,u1,v1 are_Ort_wrt w,y iff PProJ(w,y,v-u,v1-u1)=0 by A1,Th34; end;

theorem Th36: Gen w,y implies for u,v,v1 being VECTOR of V holds
 2*PProJ(w,y,u,v#v1) = PProJ(w,y,u,v)+PProJ(w,y,u,v1)
 proof assume A1: Gen w,y; let u,v,v1 be VECTOR of V;
 set a1=pr1(w,y,u),a2=pr2(w,y,u),b1=pr1(w,y,v),b2=pr2(w,y,v),
  c1=pr1(w,y,v1),c2=pr2(w,y,v1);
 thus 2*PProJ(w,y,u,v#v1) = 2*(pr1(w,y,u)*pr1(w,y,v#v1)+
 pr2(w,y,u)*pr2(w,y,v#v1))
  by Def6 .= 2*(a1*pr1(w,y,v#v1))+ 2*(a2*pr2(w,y,v#v1)) by XCMPLX_1:8 .=
 a1*(2*pr1(w,y,v#v1))+ 2*(a2*pr2(w,y,v#v1)) by XCMPLX_1:4 .=
 a1*(2*pr1(w,y,v#v1))+ a2*(2*pr2(w,y,v#v1)) by XCMPLX_1:4 .=
 a1*(b1+c1)+ a2*(2*pr2(w,y,v#v1)) by A1,Lm17 .=
 a1*(b1+c1)+ a2*(b2+c2) by A1,Lm17 .= (a1*b1+a2*b2)+(a1*c1+a2*c2)
 by Lm18 .= PProJ(w,y,u,v)+ (a1*c1+a2*c2) by Def6
 .= PProJ(w,y,u,v)+PProJ(w,y,u,v1) by Def6; end;

theorem Th37: Gen w,y implies for u,v being VECTOR of V st u<>v holds
     PProJ(w,y,u-v,u-v) <> 0
 proof assume A1: Gen w,y; let u,v be VECTOR of V; assume A2: u<>v;
 assume PProJ(w,y,u-v,u-v) = 0; then u-v,u-v are_Ort_wrt w,y by A1,Th34;
 then u-v = 0.V by A1,ANALMETR:15; hence
   contradiction by A2,RLVECT_1:35; end;

theorem Th38: Gen w,y implies for p,q,u,v,v' being VECTOR of V, A being Real st
  p,q,u,v are_DTr_wrt w,y & p<>q &
  A = (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(PProJ(w,y,p-q,p-q))" &
  v'=u+A*(p-q) holds v=v'
 proof assume A1: Gen w,y;
 let p,q,u,v,v' be VECTOR of V,A be Real;
 assume that A2: p,q,u,v are_DTr_wrt w,y and A3: p<>q and
 A4: A = (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(PProJ(w,y,p-q,p-q))" and
 A5: v'=u+A*(p-q); set s=p#q;
 A6: PProJ(w,y,p-q,p-q) <> 0 by A1,A3,Th37;
 A7: p,q // u,v' or p,q // v',u proof 1*(v'-u) = (u+A*(p-q))-u by A5,RLVECT_1:
def 9 .= A*(p-q)
  by RLSUB_2:78; then q,p // u,v' or q,p // v',u by ANALMETR:18;
  hence thesis by ANALOAF:21; end;
    (p,q,s,u#v' are_Ort_wrt w,y & u,v',s,u#v' are_Ort_wrt w,y) &
   (p,q,s,v'#u are_Ort_wrt w,y & v',u,s,v'#u are_Ort_wrt w,y)
 proof set X=PProJ(w,y,p-q,(v'#u)-s); A8: 2*X =
  2*(PProJ(w,y,p-q,v'#u)-PProJ(w,y,p-q,p#q)) by A1,Th32
  .= 2*PProJ(w,y,p-q,v'#u)-2*PProJ(w,y,p-q,p#q) by XCMPLX_1:40 .=
  (PProJ(w,y,p-q,v')+PProJ(w,y,p-q,u))-2*PProJ(w,y,p-q,p#q) by A1,Th36 .=
  (PProJ(w,y,p-q,v')+PProJ(w,y,p-q,u))-(PProJ(w,y,p-q,p)+PProJ
(w,y,p-q,q)) by A1,Th36 .=
(PProJ(w,y,p-q,u+A*(p-q)) + PProJ(w,y,p-q,u)) - PProJ
(w,y,p-q,p+q) by A1,A5,Th32 .=
  ((PProJ(w,y,p-q,u) + PProJ(w,y,p-q,A*(p-q))) + PProJ(w,y,p-q,u)) -
   PProJ(w,y,p-q,p+q) by A1,Th32;
     PProJ(w,y,p-q,A*(p-q)) =
((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(PProJ(w,y,p-q,p-q))")*PProJ
(w,y,p-q,p-q)
  by A1,A4,Th33.=
  (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*((PProJ(w,y,p-q,p-q))"*PProJ
(w,y,p-q,p-q))
  by XCMPLX_1:4
  .= (PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*1 by A6,XCMPLX_0:def 7 .=
  PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u);
  then 2*X = 0 by A8,Lm22; then X=0 by XCMPLX_1:6;
  then q,p,p#q,v'#u are_Ort_wrt w,y by A1,Th35;
  then s,v'#u,q,p are_Ort_wrt w,y by A1,Lm4;
  then A9: s,v'#u,p,q are_Ort_wrt w,y by A1,Lm4;
 set Y = PProJ(w,y,v'-u,(v'#u)-s); A10: 2*Y =
  2*(PProJ(w,y,v'-u,v'#u)-PProJ(w,y,v'-u,p#q)) by A1,Th32
  .= 2*PProJ(w,y,v'-u,v'#u)-2*PProJ(w,y,v'-u,p#q) by XCMPLX_1:40 .=
  (PProJ(w,y,v'-u,v')+PProJ(w,y,v'-u,u))-2*PProJ(w,y,v'-u,p#q) by A1,Th36 .=
  (PProJ(w,y,v'-u,v')+PProJ(w,y,v'-u,u))-(PProJ(w,y,v'-u,p)+PProJ
(w,y,v'-u,q)) by A1,Th36 .=
(PProJ(w,y,v'-u,u+A*(p-q)) + PProJ(w,y,v'-u,u)) - PProJ
(w,y,v'-u,p+q) by A1,A5,Th32.=
  ((PProJ(w,y,v'-u,u) + PProJ(w,y,v'-u,A*(p-q))) + PProJ(w,y,v'-u,u)) - PProJ
(w,y,v'-u,p+q)
  by A1,Th32;
A11:  v'-u = A*(p-q) by A5,RLSUB_2:78;
    PProJ(w,y,A*(p-q),A*(p-q)) = A*PProJ(w,y,p-q,A*(p-q)) by A1,Th33
  .= A*(((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*(PProJ(w,y,p-q,p-q))")*
   PProJ(w,y,p-q,p-q)) by A1,A4,Th33
  .= A*((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*((PProJ(w,y,p-q,p-q))"*
   PProJ(w,y,p-q,p-q))) by XCMPLX_1:4
  .= A*((PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u))*1) by A6,XCMPLX_0:def 7 .=
  A*(PProJ(w,y,p-q,p+q) - 2*PProJ(w,y,p-q,u)); then 2*Y =
((PProJ(w,y,A*(p-q),u) + (A*PProJ(w,y,p-q,p+q) - A*(2*PProJ(w,y,p-q,u)))) +
    PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by A10,A11,XCMPLX_1:40 .=
   ((PProJ(w,y,A*(p-q),u) + (PProJ(w,y,A*(p-q),p+q) - A*(2*PProJ
(w,y,p-q,u)))) +
    PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by A1,Th33 .=
((PProJ(w,y,A*(p-q),u) + (PProJ(w,y,A*(p-q),p+q) - 2*(A*PProJ(w,y,p-q,u)))) +
    PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by XCMPLX_1:4 .=
   ((PProJ(w,y,A*(p-q),u) + (PProJ(w,y,A*(p-q),p+q) - 2*PProJ
(w,y,A*(p-q),u))) +
    PProJ(w,y,A*(p-q),u)) - PProJ(w,y,A*(p-q),p+q) by A1,Th33
    .= 0 by Lm22; then A12: Y=0 by XCMPLX_1:6;
   then u,v',s,v'#u are_Ort_wrt w,y by A1,Th35
; then s,v'#u,u,v' are_Ort_wrt w,y
   by A1,Lm4; then s,v'#u,v',u are_Ort_wrt w,y by A1,Lm4;
 hence thesis by A1,A9,A12,Lm4,Th35; end;
  then p,q,u,v' are_DTr_wrt w,y or p,q,v',u are_DTr_wrt w,y by A7,Def3;
 hence v = v' by A1,A2,A3,Th27; end;

Lm25: Gen w,y implies for u,u',u1,u2,t1,t2 being VECTOR of V, A1,A2 being Real
  st u<>u' &
     A1 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1))*((PProJ
(w,y,u-u',u-u'))") &
     A2 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2))*((PProJ
(w,y,u-u',u-u'))") &
     t1 = u1+A1*(u-u') & t2 = u2+A2*(u-u')
  holds t2-t1 = (u2 - u1)+(A2-A1)*(u-u') &
  A2-A1 = ((-2)*PProJ(w,y,u-u',u2-u1))*((PProJ(w,y,u-u',u-u'))")
 proof assume A1: Gen w,y;
 let u,u',u1,u2,t1,t2 be VECTOR of V, A1,A2 be Real such that u<>u' and
 A2: A1 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1))*((PProJ
(w,y,u-u',u-u'))") and
 A3: A2 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2))*((PProJ
(w,y,u-u',u-u'))") and
 A4: t1 = u1+A1*(u-u') & t2 = u2+A2*(u-u');
thus t2-t1 = (u2 - u1)+(A2-A1)*(u-u') &
  A2-A1 = ((-2)*PProJ(w,y,u-u',u2-u1))*((PProJ(w,y,u-u',u-u'))") proof
 set uu = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2)) -
  (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1));
    uu = (-2)*PProJ(w,y,u-u',u2-u1) proof
 A5: uu = (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u2)) -
   (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1)) by A1,Th33 .=
  (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u2)) -
   (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u1)) by A1,Th33 .=
  PProJ(w,y,u-u',2*u1) - PProJ(w,y,u-u',2*u2) by Lm24 .=
   PProJ(w,y,u-u',2*u1 - 2*u2) by A1,Th32;
    2*u1 - 2*u2 = 2*u1 + -2*u2 by RLVECT_1:def 11
  .= -(2*u2 - 2*u1) by RLVECT_1:47 .= -(2*(u2 - u1))
  by RLVECT_1:48 .= 2*(-(u2 - u1)) by RLVECT_1:39 .=
  (-2)*(u2 - u1) by RLVECT_1:38; hence
   uu = (-2)*PProJ(w,y,u-u',u2 - u1)
  by A1,A5,Th33; end;
 hence thesis by A2,A3,A4,Lm23,XCMPLX_1:40; end; end;

theorem Th39:
Gen w,y implies for u,u',u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of V
  st u<>u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
 u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y &
 u1,u2 // v1,v2 holds t1,t2 // w1,w2 proof assume A1: Gen w,y;
  let u,u',u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V such that A2: u<>u' and
  A3: u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
   u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y and
  A4: u1,u2 // v1,v2; set
  A1 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1))*(PProJ(w,y,u-u',u-u'))",
  A2 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2))*(PProJ(w,y,u-u',u-u'))",
  A3 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1))*(PProJ(w,y,u-u',u-u'))",
  A4 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v2))*(PProJ(w,y,u-u',u-u'))";
 A5: (u1+A1*(u-u'))=t1 & (u2+A2*(u-u'))=t2 & (v1+A3*(u-u'))=w1 &
(v2+A4*(u-u'))=w2 by A1,A2,A3,Th38;
 A6: t1=u1+A1*(u-u') & t2=u2+A2*(u-u') by A1,A2,A3,Th38;
 A7: now assume u1=u2; then t1=t2 by A1,A2,A3,Th26;
  hence t1,t2 // w1,w2 by ANALOAF:def 1; end;
 A8: now assume v1=v2; then w1=w2 by A1,A2,A3,Th26;
  hence t1,t2 // w1,w2 by ANALOAF:def 1; end;
    now assume u1<>u2 & v1<>v2; then consider a,b such that
  A9: a*(u2-u1) = b*(v2-v1) & 0<a & 0<b by A4,ANALOAF:16;
  set uu = ((-2)*PProJ(w,y,u-u',u2-u1));
  set vv = ((-2)*PProJ(w,y,u-u',v2-v1));
  set cc = (PProJ(w,y,u-u',u-u'))";
  A10: a*uu = b*vv proof thus
     a*uu = (-2)*(a*PProJ(w,y,u-u',u2-u1)) by XCMPLX_1:4
 .= (-2)*PProJ(w,y,u-u',b*(v2-v1)) by A1,A9,Th33
    .= (-2)*(b*PProJ(w,y,u-u',v2-v1)) by A1,Th33 .=b*vv by XCMPLX_1:4; end;
  A11: a*(A2-A1) = b*(A4-A3) proof thus
    a*(A2-A1) = a*(uu*cc) by A1,A2,A6,Lm25
 .= (b*vv)*cc by A10,XCMPLX_1:4
  .= b*(vv*cc) by XCMPLX_1:4 .= b*(A4-A3) by A1,A2,A5,Lm25; end;
  A12: t2-t1 = (u2 - u1)+(A2-A1)*(u-u') by A1,A2,A5,Lm25;
  A13: w2-w1 = (v2 - v1)+(A4-A3)*(u-u') by A1,A2,A5,Lm25;
     a*(t2-t1) = a*(u2 - u1) +
   a*((A2-A1)*(u-u')) by A12,RLVECT_1:def 9
 .= b*(v2-v1) + (b*(A4-A3))*(u-u') by A9,A11,RLVECT_1:def 9 .= b*(v2 - v1) +
   b*((A4-A3)*(u-u')) by RLVECT_1:def 9 .= b*(w2-w1) by A13,RLVECT_1:def 9;
 hence t1,t2 // w1,w2 by A9,ANALOAF:def 1; end;
 hence t1,t2 // w1,w2 by A7,A8; end;

theorem Gen w,y implies for u,u',u1,u2,v1,t1,t2,w1 being VECTOR of V
 st u<>u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
  u,u',v1,w1 are_DTr_wrt w,y & v1=u1#u2 holds w1 = t1#t2
 proof assume A1: Gen w,y;
 let u,u',u1,u2,v1,t1,t2,w1 be VECTOR of V such that A2: u<>u' and
 A3: u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
  u,u',v1,w1 are_DTr_wrt w,y and A4: v1=u1#u2; set
  A1 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1))*(PProJ(w,y,u-u',u-u'))",
  A2 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2))*(PProJ(w,y,u-u',u-u'))",
  A3 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1))*(PProJ(w,y,u-u',u-u'))";
 A5: (u1+A1*(u-u'))=t1 & (u2+A2*(u-u'))=t2 & (v1+A3*(u-u'))
=w1 by A1,A2,A3,Th38;
 then A6: t1+t2 =
  A1*(u-u')+(u1 + (u2+A2*(u-u'))) by RLVECT_1:def 6 .=
  A1*(u-u')+((u1 + u2)+A2*(u-u')) by RLVECT_1:def 6 .=
  (u1 + u2)+(A1*(u-u')+A2*(u-u')) by RLVECT_1:def 6 .=
  (u1 + u2)+(A1+A2)*(u-u') by RLVECT_1:def 9 .= (v1 + v1)+(A1+A2)*(u-u') by A4,
Def2;
 A7: w1+w1 = A3*(u-u')+(v1 + (v1+A3*(u-u'))) by A5,RLVECT_1:def 6 .=
  A3*(u-u')+((v1 + v1)+A3*(u-u')) by RLVECT_1:def 6 .=
  (v1 + v1)+(A3*(u-u')+A3*(u-u')) by RLVECT_1:def 6 .=
  (v1 + v1)+(A3+A3)*(u-u') by RLVECT_1:def 9;
 A8: A3+A3 = ((PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1)) +
     (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1)))*(PProJ
(w,y,u-u',u-u'))" by XCMPLX_1:8;
 set uu = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1)) +
                        (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2)),
     vv = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1)) +
                        (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1));
 A9: uu = (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u1)) +
      (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2)) by A1,Th33 .=
 (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u1)) +
  (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u2)) by A1,Th33 .=
  (PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*u1)) +
   (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*u2)) by XCMPLX_0:def 8 .=
 (PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*u1)) +
  (PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*u2)) by XCMPLX_0:def 8 .=
PProJ(w,y,u-u',u+u') + ((PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*u1))
   + -PProJ(w,y,u-u',2*u2)) by XCMPLX_1:1 .=
 PProJ(w,y,u-u',u+u') + (PProJ(w,y,u-u',u+u') +
   (-PProJ(w,y,u-u',2*u1) + -PProJ(w,y,u-u',2*u2))) by XCMPLX_1:1 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
  (-PProJ(w,y,u-u',2*u1) + -PProJ(w,y,u-u',2*u2)) by XCMPLX_1:1 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u'))
  + -(PProJ(w,y,u-u',2*u1) + PProJ(w,y,u-u',2*u2)) by XCMPLX_1:140 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
  -(2*PProJ(w,y,u-u',u1) + PProJ(w,y,u-u',2*u2)) by A1,Th33 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
  -(2*PProJ(w,y,u-u',u1) + 2*PProJ(w,y,u-u',u2)) by A1,Th33 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
  -(2*(PProJ(w,y,u-u',u1) + PProJ(w,y,u-u',u2))) by XCMPLX_1:8 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) + -(2*(PProJ
(w,y,u-u',u1+u2))) by A1,Th32;
   vv = uu proof thus vv = (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*v1)) +
   (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1)) by A1,Th33 .=
  (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*v1)) +
   (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*v1)) by A1,Th33 .=
  (PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*v1)) +
   (PProJ(w,y,u-u',u+u') - PProJ(w,y,u-u',2*v1)) by XCMPLX_0:def 8 .=
  (PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*v1)) +
   (PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*v1)) by XCMPLX_0:def 8 .=
PProJ(w,y,u-u',u+u') + ((PProJ(w,y,u-u',u+u') + -PProJ(w,y,u-u',2*v1)) +
   -PProJ(w,y,u-u',2*v1)) by XCMPLX_1:1 .=
  PProJ(w,y,u-u',u+u') + (PProJ(w,y,u-u',u+u') +
   (-PProJ(w,y,u-u',2*v1) + -PProJ(w,y,u-u',2*v1))) by XCMPLX_1:1 .=
 (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
   (-PProJ(w,y,u-u',2*v1) + -PProJ(w,y,u-u',2*v1)) by XCMPLX_1:1 .=
  (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
   -(PProJ(w,y,u-u',2*v1) + PProJ(w,y,u-u',2*v1)) by XCMPLX_1:140 .=
  (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
   -(2*PProJ(w,y,u-u',v1) + PProJ(w,y,u-u',2*v1)) by A1,Th33 .=
  (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
   -(2*PProJ(w,y,u-u',v1) + 2*PProJ(w,y,u-u',v1)) by A1,Th33 .=
  (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
   -(2*(PProJ(w,y,u-u',v1) + PProJ(w,y,u-u',v1))) by XCMPLX_1:8 .=
  (PProJ(w,y,u-u',u+u') + PProJ(w,y,u-u',u+u')) +
   -(2*(PProJ(w,y,u-u',v1+v1))) by A1,Th32 .=uu by A4,A9,Def2; end;
 then t1+t2 = w1+w1 by A6,A7,A8,XCMPLX_1:8; hence w1=t1#t2 by Def2; end;

theorem Th41: Gen w,y implies for u,u',u1,u2,t1,t2 being VECTOR of V
 st u<>u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y
  holds u,u',u1#u2,t1#t2 are_DTr_wrt w,y
 proof assume A1: Gen w,y; let u,u',u1,u2,t1,t2 be VECTOR of V such that
 A2: u<>u' and A3: u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y;
   u1,t1,u2,t2 are_DTr_wrt w,y & u2,t2,u1,t1 are_DTr_wrt w,y
  by A1,A2,A3,Th21;
 then A4: u1,t1,u1#u2,t1#t2 are_DTr_wrt w,y & u2,t2,u2#u1,t2#t1 are_DTr_wrt w,y
  by A1,Th28;
 A5: now assume A6: u1<>t1; u1,t1,u,u' are_DTr_wrt w,y by A1,A3,Th23;
  hence thesis by A1,A4,A6,Th21; end;
 A7: now assume A8: u2<>t2; u2,t2,u,u' are_DTr_wrt w,y by A1,A3,Th23;
  hence thesis by A1,A4,A8,Th21; end;
    now assume A9: u1=t1 & u2=t2;
  then A10: u,u' // u1#u2,t1#t2 by ANALOAF:18;
     u#u',(u1#u2)#(t1#t2),u1#u2,t1#t2 are_Ort_wrt w,y by A1,A9,Lm5;
  then A11: u1#u2,t1#t2,u#u',(u1#u2)#(t1#t2) are_Ort_wrt w,y by A1,Lm4;
     u,u',u#u',u1#u2 are_Ort_wrt w,y proof set uu'=u#u';
     u,u',uu',u1#t1 are_Ort_wrt w,y & u,u',uu',u2#t2 are_Ort_wrt w,y by A3,Def3
; then A12: u'-u,u1-uu' are_Ort_wrt w,y &
   u'-u,u2-uu' are_Ort_wrt w,y by A9,ANALMETR:def 3;
   A13: u1#u2-uu' = (2")*(u1-uu')+(2")*(u2-uu') proof
    A14: 2*(u1#u2) = (1+1)*(u1#u2) .= 1*(u1#u2)+1*(u1#u2) by RLVECT_1:def 9
    .= (u1#u2)+1*(u1#u2) by RLVECT_1:def 9 .= (u1#u2)+(u1#u2) by RLVECT_1:def 9
    .=u1+u2 by Def2;
    A15: -(2*uu') = -((1+1)*uu') .= -(1*uu'+1*uu') by RLVECT_1:def 9 .=
     -(uu' + 1*uu') by RLVECT_1:def 9 .= -(uu'+uu') by RLVECT_1:def 9
     .= -uu' + -uu' by Lm19;
      u1#u2-uu' = (2"*2)*(u1#u2-uu') by RLVECT_1:def 9
 .= 2"*(2*(u1#u2-uu')) by RLVECT_1:def 9 .=
2"*((u1+u2)-(2*uu')) by A14,RLVECT_1:48 .=2"*((u1+u2)+(-uu'+ -uu')) by A15,
RLVECT_1:def 11
    .= 2"*(((u1+u2)+ -uu') + -uu') by RLVECT_1:def 6 .=
    2"*(((-uu' + u1)+u2) + -uu') by RLVECT_1:def 6 .=
    2"*(((u1-uu')+u2) + -uu') by RLVECT_1:def 11 .=
    2"*((u1-uu')+(u2 + -uu')) by RLVECT_1:def 6 .=
    2"*((u1-uu')+(u2-uu')) by RLVECT_1:def 11 .=
    2"*(u1-uu')+2"*(u2-uu') by RLVECT_1:def 9; hence thesis; end;
     u'-u,(2")*(u1-uu') are_Ort_wrt w,y & u'-u,(2")*(u2-uu') are_Ort_wrt w,y
   by A12,ANALMETR:11; then u'-u,u1#u2-uu' are_Ort_wrt w,y
   by A1,A13,ANALMETR:14; hence thesis by ANALMETR:def 3; end;
  hence thesis by A9,A10,A11,Def3; end;
 hence thesis by A5,A7; end;

theorem Th42: Gen w,y implies for u,u',u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of
V
   st u<>u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
 u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y
 & u1,u2,v1,v2 are_Ort_wrt w,y holds t1,t2,w1,w2 are_Ort_wrt w,y
 proof assume A1: Gen w,y;
 let u,u',u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V such that A2: u<>u' and
 A3: u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
 u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y and
 A4: u1,u2,v1,v2 are_Ort_wrt w,y; set
  A1 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u1))*(PProJ(w,y,u-u',u-u'))",
  A2 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',u2))*(PProJ(w,y,u-u',u-u'))",
  A3 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v1))*(PProJ(w,y,u-u',u-u'))",
  A4 = (PProJ(w,y,u-u',u+u') - 2*PProJ(w,y,u-u',v2))*(PProJ(w,y,u-u',u-u'))";
 A5: (u1+A1*(u-u'))=t1 & (u2+A2*(u-u'))=t2 & (v1+A3*(u-u'))=w1 &
(v2+A4*(u-u'))=w2 by A1,A2,A3,Th38;
 A6: t1=u1+A1*(u-u') & t2=u2+A2*(u-u') by A1,A2,A3,Th38;
 A7: PProJ(w,y,u-u',u-u') <> 0 by A1,A2,Th37;
 A8: t2-t1 = (u2 - u1)+(A2-A1)*(u-u') by A1,A2,A5,Lm25;
    w2-w1 = (v2 - v1)+(A4-A3)*(u-u') by A1,A2,A5,Lm25;
 then A9: PProJ(w,y,t2-t1,w2-w1) =PProJ(w,y,u2-u1,(v2 - v1)+(A4-A3)*(u-u')) +
   PProJ(w,y,(A2-A1)*(u-u'),(v2 - v1)+(A4-A3)*(u-u')) by A1,A8,Th32 .=
  (PProJ(w,y,u2-u1,v2-v1) + PProJ(w,y,u2-u1,(A4-A3)*(u-u'))) +
   PProJ(w,y,(A2-A1)*(u-u'),(v2 - v1)+(A4-A3)*(u-u')) by A1,Th32 .=
  (0 + PProJ(w,y,u2-u1,(A4-A3)*(u-u'))) +
   PProJ(w,y,(A2-A1)*(u-u'),(v2 - v1)+(A4-A3)*(u-u')) by A1,A4,Th35 .=
  PProJ(w,y,u2-u1,(A4-A3)*(u-u')) +
   (PProJ(w,y,(A2-A1)*(u-u'),(v2 - v1)) + PProJ
(w,y,(A2-A1)*(u-u'),(A4-A3)*(u-u')))
   by A1,Th32;
 A10: (-2)*(-2) = 4;
 set aa = (PProJ(w,y,u-u',u-u'))"*((PProJ(w,y,u-u',u2-u1)*PProJ
(w,y,u-u',v2-v1)));
 A11: PProJ(w,y,(A2-A1)*(u-u'),(A4-A3)*(u-u')) =
  (A2-A1)*PProJ(w,y,u-u',(A4-A3)*(u-u')) by A1,Th33 .=
  (A2-A1)*((A4-A3)*PProJ(w,y,u-u',u-u')) by A1,Th33 .=
  (A2-A1)*( (((-2)*PProJ(w,y,u-u',v2-v1)) * ((PProJ(w,y,u-u',u-u'))") ) *
   PProJ(w,y,u-u',u-u') ) by A1,A2,A5,Lm25 .=
  (A2-A1)*( ((-2)*PProJ(w,y,u-u',v2-v1))*(((PProJ(w,y,u-u',u-u'))" )*
   PProJ(w,y,u-u',u-u')) ) by XCMPLX_1:4 .=
  (A2-A1)*( ((-2)*PProJ(w,y,u-u',v2-v1))*1 ) by A7,XCMPLX_0:def 7 .=
((-2)*(A2-A1))*PProJ(w,y,u-u',v2-v1) by XCMPLX_1:4 .=
  ((-2)*( ((-2)*PProJ(w,y,u-u',u2-u1))*((PProJ(w,y,u-u',u-u'))")) )*
   PProJ(w,y,u-u',v2-v1) by A1,A2,A6,Lm25 .=
  ((-2)*( (-2)*(PProJ(w,y,u-u',u2-u1)*((PProJ(w,y,u-u',u-u'))"))) )*
   PProJ(w,y,u-u',v2-v1) by XCMPLX_1:4 .=
(4*(PProJ(w,y,u-u',u2-u1)*((PProJ(w,y,u-u',u-u'))")))*
   PProJ(w,y,u-u',v2-v1) by A10,XCMPLX_1:4 .=
4*(( ((PProJ(w,y,u-u',u-u'))") * PProJ(w,y,u-u',u2-u1) )*
   PProJ(w,y,u-u',v2-v1)) by XCMPLX_1:4 .=4*aa by XCMPLX_1:4;
 A12:  PProJ(w,y,u2-u1,(A4-A3)*(u-u')) = PProJ
(w,y,u2-u1,u-u')*(A4-A3) by A1,Th33 .=
  PProJ(w,y,u2-u1,u-u')*( ((-2)*PProJ(w,y,u-u',v2-v1))*
   ((PProJ(w,y,u-u',u-u'))") ) by A1,A2,A5,Lm25 .=
  PProJ(w,y,u2-u1,u-u')*( (-2)*(PProJ(w,y,u-u',v2-v1)*
   ((PProJ(w,y,u-u',u-u'))")) ) by XCMPLX_1:4 .=
(-2)*(PProJ(w,y,u2-u1,u-u')*(((PProJ(w,y,u-u',u-u'))"*
   PProJ(w,y,u-u',v2-v1))) ) by XCMPLX_1:4 .=
  (-2)*( (PProJ(w,y,u-u',u-u'))"*((PProJ(w,y,u2-u1,u-u')*
   PProJ(w,y,u-u',v2-v1))) ) by XCMPLX_1:4 .=(-2)*aa by Th31;
     PProJ(w,y,(A2-A1)*(u-u'),(v2 - v1)) =
  PProJ(w,y,v2-v1,(A2-A1)*(u-u')) by Th31 .=
  PProJ(w,y,v2-v1,u-u')*(A2-A1) by A1,Th33 .=
  PProJ(w,y,v2-v1,u-u')*( ((-2)*PProJ(w,y,u-u',u2-u1))*
   ((PProJ(w,y,u-u',u-u'))") ) by A1,A2,A6,Lm25 .=
  PProJ(w,y,v2-v1,u-u')*( (-2)*(PProJ(w,y,u-u',u2-u1)*
   ((PProJ(w,y,u-u',u-u'))")) ) by XCMPLX_1:4 .=
(-2)*( PProJ(w,y,v2-v1,u-u')*(((PProJ(w,y,u-u',u-u'))"*
   PProJ(w,y,u-u',u2-u1))) ) by XCMPLX_1:4 .=
  (-2)*( (PProJ(w,y,u-u',u-u'))"*((PProJ(w,y,v2-v1,u-u')*
   PProJ(w,y,u-u',u2-u1))) ) by XCMPLX_1:4 .=(-2)*aa by Th31;
 then PProJ(w,y,t2-t1,w2-w1) = (-2)*aa + (((-2)+4)*aa) by A9,A11,A12,XCMPLX_1:8
  .= ((-2)+((-2)+4))*aa by XCMPLX_1:8
  .= 0; hence t1,t2,w1,w2 are_Ort_wrt w,y by A1,Th35; end;

theorem Th43: for u,u',u1,u2,v1,v2,t1,t2,w1,w2 being VECTOR of V holds
 (Gen w,y & u<>u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y &
  u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y
  & u1,u2,v1,v2 are_DTr_wrt w,y implies t1,t2,w1,w2 are_DTr_wrt w,y)
proof let u,u',u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V; assume that
 A1: Gen w,y and A2: u<>u' and A3: u,u',u1,t1 are_DTr_wrt w,y &
 u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y &
 u,u',v2,w2 are_DTr_wrt w,y and A4: u1,u2,v1,v2 are_DTr_wrt w,y;
A5: t1,t2 // w1,w2 proof u1,u2 // v1,v2 by A4,Def3;
  hence thesis by A1,A2,A3,Th39; end;
 set uu=u1#u2,vv=v1#v2;
A6: u,u',uu,(t1#t2) are_DTr_wrt w,y & u,u',vv,(w1#w2)
 are_DTr_wrt w,y by A1,A2,A3,Th41;
    u1,u2,uu,vv are_Ort_wrt w,y by A4,Def3;
then A7: t1,t2,t1#t2,w1#w2 are_Ort_wrt w,y by A1,A2,A3,A6,Th42;
     v1,v2,uu,vv are_Ort_wrt w,y by A4,Def3;
 then w1,w2,t1#t2,w1#w2 are_Ort_wrt w,y by A1,A2,A3,A6,Th42;
hence t1,t2,w1,w2 are_DTr_wrt w,y by A5,A7,Def3; end;

definition let V; let w,y;
 func DTrapezium(V,w,y) -> Relation of [:the carrier of V,the carrier of V:]
 means :Def7:  [x,z] in it iff
     ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_DTr_wrt w,y;
existence proof set VV = [:the carrier of V,the carrier of V:];
  defpred P[set,set] means ex u,u1,v,v1 st $1=[u,u1] & $2=[v,v1] &
                     u,u1,v,v1 are_DTr_wrt w,y;
consider P being Relation of VV,VV such that A1: [x,z] in P iff
      x in VV & z in VV & P[x,z] from Rel_On_Set_Ex;
 take P; let x,z; thus [x,z] in P implies ex u,u1,v,v1 st x=[u,u1] & z=[v,v1]
  & u,u1,v,v1 are_DTr_wrt w,y by A1; assume
    ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_DTr_wrt w,y;
                       hence [x,z] in P by A1; end;
uniqueness proof let P,Q be Relation of [:the carrier of V,the carrier of V:]
   such that
  A2:  [x,z] in P iff
    ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_DTr_wrt w,y and
  A3:  [x,z] in Q iff
    ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_DTr_wrt w,y;
    for x,z holds [x,z] in P iff [x,z] in Q
  proof let x,z; [x,z] in P iff
  ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_DTr_wrt w,y by A2;
  hence thesis by A3; end; hence thesis by RELAT_1:def 2; end; end;

theorem Th44:  [[u,v],[u1,v1]] in DTrapezium(V,w,y)
 iff u,v,u1,v1 are_DTr_wrt w,y proof
   now assume [[u,v],[u1,v1]] in DTrapezium(V,w,y);
 then consider u',v',u1',v1' being VECTOR of V such that
 A1: [u,v]=[u',v'] & [u1,v1]=[u1',v1'] and A2: u',v',u1',v1' are_DTr_wrt w,y
 by Def7; u=u' & v=v' & u1=u1' & v1=v1' by A1,ZFMISC_1:33;
 hence u,v,u1,v1 are_DTr_wrt w,y by A2; end;
hence thesis by Def7; end;

definition let V;
  func MidPoint(V) -> BinOp of the carrier of V means
 :Def8: for u,v holds it.(u,v) = u#v;
existence
proof
  deffunc F(VECTOR of V,VECTOR of V) = $1#$2;
  ex B being BinOp of the carrier of V st
   for u,v holds B.(u,v) = F(u,v) from BinOpLambda;
  hence thesis;
end;
uniqueness
proof
  deffunc F(VECTOR of V,VECTOR of V) = $1#$2;
  for o1,o2 being BinOp of the carrier of V st
    (for a,b being Element of V holds o1.(a,b) = F(a,b)) &
    (for a,b being Element of V holds o2.(a,b) = F(a,b))
  holds o1 = o2 from BinOpDefuniq;
  hence thesis;
end;
end;

definition
  struct(AffinStruct,MidStr) AfMidStruct (# carrier -> set,
                    MIDPOINT -> BinOp of the carrier,
                    CONGR -> Relation of [:the carrier,the carrier:] #);
end;

definition
 cluster non empty strict AfMidStruct;
 existence
  proof
   consider D being non empty set, m being BinOp of D,
            c being Relation of [:D,D:];
   take AfMidStruct (#D,m,c #);
   thus the carrier of AfMidStruct (#D,m,c #) is non empty;
   thus thesis;
  end;
end;

definition let V,w,y;
  func DTrSpace(V,w,y) -> strict AfMidStruct equals :Def9:
  AfMidStruct(#the carrier of V, MidPoint(V),DTrapezium(V,w,y)#);
correctness; end;

definition let V,w,y;
 cluster DTrSpace(V,w,y) -> non empty;
 coherence
  proof
     DTrSpace(V,w,y) =
    AfMidStruct(#the carrier of V, MidPoint(V),DTrapezium(V,w,y)#) by Def9;
   hence the carrier of DTrSpace(V,w,y) is non empty;
  end;
end;

definition let AMS be AfMidStruct;
  func Af(AMS) -> strict AffinStruct equals
 :Def10:  AffinStruct(#the carrier of AMS, the CONGR of AMS#);
 correctness; end;

definition let AMS be non empty AfMidStruct;
 cluster Af(AMS) -> non empty;
 coherence
  proof
     Af(AMS) = AffinStruct(#the carrier of AMS, the CONGR of AMS#) by Def10;
   hence the carrier of Af(AMS) is non empty;
  end;
end;

definition
 let AMS be non empty AfMidStruct, a,b be Element of AMS;
 canceled;

 func a#b -> Element of AMS equals
 :Def12:  (the MIDPOINT of AMS).(a,b); correctness; end;

reserve a,b,c,d,a1,a2,b1,c1,d1,d2,p,q
                       for Element of DTrSpace(V,w,y);

canceled;

theorem Th46: for x being set holds x is Element of the
 carrier of DTrSpace(V,w,y) iff x is VECTOR of V
 proof let x be set;
   (DTrSpace(V,w,y))
 = AfMidStruct(#the carrier of V, MidPoint(V),DTrapezium(V,w,y)#) by Def9;
 hence thesis; end;

theorem Th47: Gen w,y & u=a & v=b & u1=a1 & v1=b1 implies
                   (a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y)
 proof assume A1: Gen w,y & u=a & v=b & u1=a1 & v1=b1; A2:
 DTrSpace(V,w,y) =
  AfMidStruct(#the carrier of V, MidPoint(V),DTrapezium(V,w,y)#) by Def9;
  A3: now assume a,b // a1,b1;
   then [[a,b],[a1,b1]] in DTrapezium(V,w,y) by A2,ANALOAF:def 2;
   hence u,v,u1,v1 are_DTr_wrt w,y by A1,Th44; end;
     now assume u,v,u1,v1 are_DTr_wrt w,y;
   then [[a,b],[a1,b1]] in DTrapezium(V,w,y) by A1,Th44;
   hence a,b // a1,b1 by A2,ANALOAF:def 2; end;
hence thesis by A3; end;

theorem Th48: Gen w,y & u=a & v=b implies u#v = a#b
 proof assume A1: Gen w,y & u=a & v=b;
  (DTrSpace(V,w,y))=AfMidStruct(#the carrier of V, MidPoint(V),DTrapezium(V,w,y
)
  #) by Def9;
 hence a#b = (MidPoint(V)).(u,v) by A1,Def12 .= u#v by Def8; end;

Lm26: Gen w,y & a,b // b,c implies a=b & b=c
 proof assume A1: Gen w,y & a,b // b,c; reconsider u=a,v=b,u1=c as
 VECTOR of V by Th46; u,v,v,u1 are_DTr_wrt w,y by A1,Th47;hence thesis by A1,
Th20; end;

Lm27: Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1
 proof assume A1: Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a<>b;
 reconsider u=a,v=b,u1=a1,v1=b1,u2=c1,v2=d1 as VECTOR of V by Th46;
   u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y & u<>v by A1,Th47;
 then u1,v1,u2,v2 are_DTr_wrt w,y by A1,Th21; hence thesis by A1,Th47; end;

Lm28: Gen w,y & a,b // c,d implies c,d // a,b & b,a // d,c
 proof assume A1: Gen w,y & a,b // c,d;
 reconsider u=a,v=b,u1=c,v1=d as VECTOR of V by Th46;
   u,v,u1,v1 are_DTr_wrt w,y by A1,Th47; then v,u,v1,u1 are_DTr_wrt w,y &
 u1,v1,u,v are_DTr_wrt w,y by A1,Th23,Th24; hence thesis by A1,Th47; end;

Lm29: Gen w,y implies ex d st a,b // c,d or a,b // d,c
 proof assume A1: Gen w,y; reconsider u=a,v=b,u1=c as VECTOR of V by Th46;
 consider t being VECTOR of V such that
 A2: u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y by A1,Th22;
 reconsider d=t as Element of DTrSpace(V,w,y) by Th46;
   a,b // c,d or a,b // d,c by A1,A2,Th47; hence thesis; end;

Lm30: Gen w,y & a,b // c,d1 & a,b // c,d2 implies a=b or d1=d2
 proof assume A1: Gen w,y & a,b // c,d1 & a,b // c,d2;
 reconsider u=a,v=b,u1=c,v1=d1,v2=d2 as VECTOR of V by Th46;
   u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y by A1,Th47;
 hence thesis by A1,Th26; end;

Lm31: Gen w,y implies a#b = b#a
 proof assume A1: Gen w,y; reconsider u=a,v=b as VECTOR of V by Th46;
 thus a#b = u#v by A1,Th48 .= b#a by A1,Th48; end;

Lm32: Gen w,y implies a#a = a
 proof assume A1: Gen w,y; reconsider u=a as VECTOR of V by Th46;
   u#u = u; hence thesis by A1,Th48; end;

Lm33: Gen w,y implies (a#b)#(c#d) = (a#c)#(b#d)
 proof assume A1: Gen w,y; reconsider u=a,u1=b,v=c,v1=d as VECTOR of V by Th46
; set ab=a#b,cd=c#d,ac=a#c,bd=b#d,uu1=u#u1,vv1=v#v1,uv=u#v,u1v1=u1#v1;
 A2: ab=uu1 & cd=vv1 & ac = uv & bd=u1v1 by A1,Th48; hence (ab)#(cd) =
 (uu1)#(vv1) by A1,Th48 .= (uv)#(u1v1) by Th8 .= (ac)#(bd) by A1,A2,Th48; end;

Lm34: Gen w,y implies ex p st p#a=b
 proof assume A1: Gen w,y; reconsider u=a,v=b as VECTOR of V by Th46;
 consider u1 such that A2: u#u1=v by Th7;
 reconsider p=u1 as Element of DTrSpace(V,w,y) by Th46; p#a= u
#
u1 by A1,Th48; hence thesis by A2; end;

Lm35: Gen w,y & a#a1=a#a2 implies a1=a2
 proof assume A1: Gen w,y & a#a1=a#a2; reconsider u=a,u1=a1,u2=a2 as
 VECTOR of V by Th46; u#u1=a#a1 & u#u2=a#a2 by A1,Th48;
 hence thesis by A1,Th9; end;

Lm36: Gen w,y & a,b // c,d implies a,b // (a#c),(b#d)
 proof assume that A1: Gen w,y and A2: a,b // c,d;
 reconsider u=a,v=b,u1=c,v1=d as VECTOR of V by Th46;
 A3: a#c = u#u1 & b#d = v#v1 by A1,Th48; u,v,u1,v1 are_DTr_wrt w,y by A1,A2,
Th47;
 then u,v,(u#u1),(v#v1) are_DTr_wrt w,y by A1,Th28;
 hence thesis by A1,A3,Th47; end;

Lm37: Gen w,y & a,b // c,d implies (a,b // (a#d),(b#c) or a,b // (b#c),(a#d))
 proof assume that A1: Gen w,y and A2: a,b // c,d;
 reconsider u=a,v=b,u1=c,v1=d as VECTOR of V by Th46;
 A3: a#d = u#v1 & b#c = v#u1 by A1,Th48; u,v,u1,v1 are_DTr_wrt w,y by A1,A2,
Th47;
 then u,v,(u#v1),(v#u1) are_DTr_wrt w,y or u,v,(v#u1),(u#v1) are_DTr_wrt w,y
 by A1,Th29; hence thesis by A1,A3,Th47; end;

Lm38: Gen w,y & a,b // c,d & a#a1=p & b#b1=p & c#c1=p & d#d1=p implies
 a1,b1 // c1,d1
 proof assume that A1: Gen w,y and A2: a,b // c,d and
 A3: a#a1=p & b#b1=p & c#c1=p & d#d1=p;
 reconsider u1=a,u2=b,v1=c,v2=d,u=p,t1=a1,t2=b1,w1=c1,w2=d1 as
 VECTOR of V by Th46; A4: u1,u2,v1,v2 are_DTr_wrt w,y by A1,A2,Th47;
   u=u1#t1 & u=u2#t2 & u=v1#w1 & u=v2#w2 by A1,A3,Th48;
 then t1,t2,w1,w2 are_DTr_wrt w,y by A1,A4,Th30; hence thesis by A1,Th47; end
;

Lm39: Gen w,y & p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
 a,b // c,d implies a1,b1 // c1,d1
proof assume that A1: Gen w,y and A2: p<>q and
A3: p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 and A4: a,b // c,d;
reconsider u=p,u'=q,u1=a,u2=b,v1=c,v2=d,t1=a1,t2=b1,w1=c1,w2=d1 as VECTOR
of V by Th46
; u<>u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y
 & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y
 & u1,u2,v1,v2 are_DTr_wrt w,y by A1,A2,A3,A4,Th47;
 then t1,t2,w1,w2 are_DTr_wrt w,y by A1,Th43; hence thesis by A1,Th47; end;

definition let IT be non empty AfMidStruct;
 attr IT is MidOrdTrapSpace-like means
:Def13:
for a,b,c,d,a1,b1,c1,d1,p,q being Element of IT holds
  a#b=b#a & a#a=a & (a#b)#(c#d)=(a#c)#(b#d) &
  (ex p being Element of IT st p#a=b) &
  (a#b=a#c implies b=c) & (a,b // c,d implies a,b // (a#c),(b#d)) &
  (a,b // c,d implies (a,b // (a#d),(b#c) or a,b // (b#c),(a#d))) &
  (a,b // c,d & a#a1=p & b#b1=p & c#c1=p & d#d1=p implies a1,b1 // c1,d1) &
  (p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
   a,b // c,d implies a1,b1 // c1,d1) & (a,b // b,c implies a=b & b=c) &
  (a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1) &
  (a,b // c,d implies c,d // a,b & b,a // d,c) &
  (ex d being Element of IT st a,b // c,d or a,b // d,c) &
  (a,b // c,p & a,b // c,q implies a=b or p=q);
end;

definition
 cluster strict MidOrdTrapSpace-like (non empty AfMidStruct);
existence proof consider V such that A1: ex w,y st Gen w,y by ANALMETR:7;
consider w,y being VECTOR of V such that A2: Gen w,y by A1;
set X = DTrSpace(V,w,y);
    for a,b,c,d,a1,b1,c1,d1,p,q being Element of X holds
  a#b=b#a & a#a=a & (a#b)#(c#d)=(a#c)#(b#d) &
  (ex p being Element of X st p#a=b) &
  (a#b=a#c implies b=c) & (a,b // c,d implies a,b // (a#c),(b#d)) &
  (a,b // c,d implies (a,b // (a#d),(b#c) or a,b // (b#c),(a#d))) &
  (a,b // c,d & a#a1=p & b#b1=p & c#c1=p & d#d1=p implies a1,b1 // c1,d1) &
  (p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
   a,b // c,d implies a1,b1 // c1,d1) & (a,b // b,c implies a=b & b=c) &
  (a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1) &
  (a,b // c,d implies c,d // a,b & b,a // d,c) &
  (ex d being Element of X st a,b // c,d or a,b // d,c) &
  (a,b // c,p & a,b // c,q implies a=b or p=q)
   by A2,Lm26,Lm27,Lm28,Lm29,Lm30,Lm31,Lm32,Lm33,Lm34,Lm35,Lm36,Lm37,Lm38,Lm39;
   then X is MidOrdTrapSpace-like by Def13;
  hence thesis;
 end;
end;

definition
 mode MidOrdTrapSpace is MidOrdTrapSpace-like (non empty AfMidStruct);
end;

theorem Gen w,y implies DTrSpace(V,w,y) is MidOrdTrapSpace
proof assume A1: Gen w,y; set X = DTrSpace(V,w,y);
  for a,b,c,d,a1,b1,c1,d1,p,q being Element of X holds
  a#b=b#a & a#a=a & (a#b)#(c#d)=(a#c)#(b#d) &
  (ex p being Element of X st p#a=b) &
  (a#b=a#c implies b=c) & (a,b // c,d implies a,b // (a#c),(b#d)) &
  (a,b // c,d implies (a,b // (a#d),(b#c) or a,b // (b#c),(a#d))) &
  (a,b // c,d & a#a1=p & b#b1=p & c#c1=p & d#d1=p implies a1,b1 // c1,d1) &
  (p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
   a,b // c,d implies a1,b1 // c1,d1) & (a,b // b,c implies a=b & b=c) &
  (a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1) &
  (a,b // c,d implies c,d // a,b & b,a // d,c) &
  (ex d being Element of X st a,b // c,d or a,b // d,c) &
  (a,b // c,p & a,b // c,q implies a=b or p=q) by A1,Lm26,Lm27,Lm28,Lm29,Lm30,
Lm31,Lm32,Lm33,Lm34,Lm35,Lm36,Lm37,Lm38,Lm39; hence thesis by Def13; end;
 consider MOS being MidOrdTrapSpace; set X=Af(MOS);
Lm40:now
let a,b,c,d,a1,b1,c1,d1,p,q be Element of X;
A1:X = AffinStruct(#the carrier of MOS, the CONGR of MOS#) by Def10;
A2: now let a,b,c,d be Element of X, a',b',c',d' be Element of
  the carrier of MOS such that A3: a=a' & b=b' & c =c' & d=d';
  A4: now assume a,b // c,d;
   then [[a,b],[c,d]] in the CONGR of MOS by A1,ANALOAF:def 2;
hence a',b' // c',d' by A3,ANALOAF:def 2; end;
     now assume a',b' // c',d'; then [[a,b],[c,d]] in the CONGR of MOS by A3,
ANALOAF:def 2;hence a,b // c,d by A1,ANALOAF:def 2; end;
 hence a,b // c,d iff a',b' // c',d' by A4; end;
 reconsider a'=a,b'=b,c'=c,d'=d,a1'=a1,b1'=b1,c1'=c1,d1'=d1,p'=p,q'=q as
  Element of MOS by A1;
 A5: now assume a,b // b,c; then a',b' // b',c' by A2;hence a=b & b=c by Def13
; end;
 A6: now assume a,b // a1,b1 & a,b // c1,d1 & a<>b; then a',b' // a1',b1' &
   a',b' // c1',d1' & a'<>b' by A2; then a1',b1' // c1',d1' by Def13;
   hence a1,b1 // c1,d1 by A2; end;
 A7: now assume a,b // c,d; then a',b' // c',d' by A2; then c',d' // a',b' &
   b',a' // d',c' by Def13; hence c,d // a,b & b,a // d,c by A2; end;
 A8: ex d being Element of X st a,b // c,d or a,b // d,c proof
   consider x' being Element of MOS such that
   A9: a',b' // c',x' or a',b' // x',c' by Def13; reconsider x=x' as
   Element of X by A1; take x; thus thesis by A2,A9; end;
    now assume a,b // c,p & a,b // c,q; then a',b' // c',p' & a',b' // c',q'
   by A2; hence a=b or p=q by Def13; end;
 hence (a,b // b,c implies a=b & b=c) &
  (a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1) &
  (a,b // c,d implies c,d // a,b & b,a // d,c) &
  (ex d being Element of X st a,b // c,d or a,b // d,c) &
  (a,b // c,p & a,b // c,q implies a=b or p=q) by A5,A6,A7,A8; end;

definition let IT be non empty AffinStruct;
 attr IT is OrdTrapSpace-like means :Def14:
for a,b,c,d,a1,b1,c1,d1,p,q being Element of IT holds
(a,b // b,c implies a=b & b=c) &
  (a,b // a1,b1 & a,b // c1,d1 & a<>b implies a1,b1 // c1,d1) &
  (a,b // c,d implies c,d // a,b & b,a // d,c) &
  (ex d being Element of IT st a,b // c,d or a,b // d,c) &
  (a,b // c,p & a,b // c,q implies a=b or p=q);
end;

definition
 cluster strict OrdTrapSpace-like (non empty AffinStruct);
  existence
   proof
       X is OrdTrapSpace-like by Def14,Lm40;
    hence thesis;
   end;
end;

definition
 mode OrdTrapSpace is OrdTrapSpace-like (non empty AffinStruct);
end;

definition let MOS be MidOrdTrapSpace;
  cluster Af(MOS) -> OrdTrapSpace-like;
coherence proof set X=Af(MOS);
   Af(MOS)is OrdTrapSpace-like
 proof
let a,b,c,d,a1,b1,c1,d1,p,q be Element of X;
A1:X = AffinStruct(#the carrier of MOS, the CONGR of MOS#) by Def10;
A2: now let a,b,c,d be Element of X, a',b',c',d' be Element of
  the carrier of MOS such that A3: a=a' & b=b' & c =c' & d=d';
  A4: now assume a,b // c,d;
   then [[a,b],[c,d]] in the CONGR of MOS by A1,ANALOAF:def 2;
   hence a',b' // c',d' by A3,ANALOAF:def 2; end;
     now assume a',b' // c',d'; then [[a,b],[c,d]] in the CONGR of MOS by A3,
ANALOAF:def 2;hence a,b // c,d by A1,ANALOAF:def 2; end;
 hence a,b // c,d iff a',b' // c',d' by A4; end;
 reconsider a'=a,b'=b,c'=c,d'=d,a1'=a1,b1'=b1,c1'=c1,d1'=d1,p'=p,q'=q as
  Element of MOS by A1;
 A5: now assume a,b // b,c; then a',b' // b',c' by A2;hence a=b & b=c by Def13
; end;
 A6: now assume a,b // a1,b1 & a,b // c1,d1 & a<>b; then a',b' // a1',b1' &
   a',b' // c1',d1' & a'<>b' by A2; then a1',b1' // c1',d1' by Def13;
   hence a1,b1 // c1,d1 by A2; end;
 A7: now assume a,b // c,d; then a',b' // c',d' by A2; then c',d' // a',b' &
   b',a' // d',c' by Def13; hence c,d // a,b & b,a // d,c by A2; end;
 A8: ex d being Element of X st a,b // c,d or a,b // d,c proof
   consider x' being Element of MOS such that
   A9: a',b' // c',x' or a',b' // x',c' by Def13; reconsider x=x' as
   Element of X by A1; take x; thus thesis by A2,A9; end;
    now assume a,b // c,p & a,b // c,q; then a',b' // c',p' & a',b' // c',q'
   by A2; hence a=b or p=q by Def13; end;
hence thesis by A5,A6,A7,A8; end;
  hence thesis;
 end;
end;

reserve OTS for OrdTrapSpace;
reserve a,b,c,d for Element of OTS;
reserve a',b',c',d',a1',b1',d1' for Element of Lambda(OTS);

theorem Th50: for x being set holds (x is Element of OTS iff
  x is Element of Lambda(OTS))
proof let x be set;
  Lambda(OTS) = AffinStruct (# the carrier of OTS, lambda(the CONGR of OTS) #)
by DIRAF:def 2;
hence thesis; end;

theorem Th51: a=a' & b=b' & c =c' & d=d' implies (a',b' // c',d' iff
  a,b // c,d or a,b // d,c)
proof assume A1: a=a' & b=b' & c =c' & d=d'; A2: Lambda(OTS) =
AffinStruct(#the carrier of OTS,lambda(the CONGR of OTS)#) by DIRAF:def 2;
A3: now assume a',b' // c',d';
then [[a',b'],[c',d']] in lambda(the CONGR of OTS) by A2,ANALOAF:def 2;
 then [[a,b],[c,d]] in the CONGR of OTS or [[a,b],[d,c]] in the CONGR of OTS
 by A1,DIRAF:def 1; hence a,b // c,d or a,b // d,c by ANALOAF:def 2; end;
   now assume a,b // c,d or a,b // d,c; then [[a,b],[c,d]] in the CONGR of
OTS
or
 [[a,b],[d,c]] in the CONGR of OTS by ANALOAF:def 2;
 then [[a,b],[c,d]] in the CONGR of Lambda(OTS) by A2,DIRAF:def 1;
 hence a',b' // c',d' by A1,ANALOAF:def 2; end; hence thesis by A3; end;

Lm41: for a',b',c' ex d' st a',b' // c',d'
proof let a',b',c'; reconsider a=a',b=b',c =c' as Element of OTS
by Th50; consider d such that A1: a,b // c,d or a,b // d,c by Def14;
reconsider d'=d as Element of Lambda(OTS) by Th50; take d';
thus a',b' // c',d' by A1,Th51; end;

Lm42: a',b' // c',d' implies c',d' // a',b'
proof assume A1: a',b' // c',d'; reconsider a=a',b=b',c =c',d=d' as Element of
the carrier of OTS by Th50;
A2: now assume a,b // c,d; then c,d // a,b by Def14;
 hence c',d' // a',b' by Th51; end;
   now assume a,b // d,c; then b,a // c,d by Def14; then c,d // b,a by Def14
; hence c',d' // a',b' by Th51; end;
hence thesis by A1,A2,Th51; end;

Lm43: a1'<>b1' & a1',b1' // a',b' & a1',b1' // c',d' implies a',b' // c',d'
proof assume that A1: a1'<>b1' and A2: a1',b1' // a',b' & a1',b1' // c',d';
reconsider a1=a1',b1=b1',a=a',b=b',c =c',d=d' as Element of OTS
by Th50; (a1,b1 // a,b or a1,b1 // b,a) & (a1,b1 // c,d or a1,b1 // d,c)
by A2,Th51; then a,b // c,d or a,b // d,c or b,a // c,d or b,a // d,c
by A1,Def14; then a,b // c,d or a,b // d,c by Def14;
hence thesis by Th51; end;

Lm44: a',b' // c',d' & a',b' // c',d1' implies a'=b' or d'=d1'
proof assume A1: a',b' // c',d' & a',b' // c',d1'; assume A2: a'<>b';
reconsider a=a',b=b',c =c',d=d',d1=d1' as Element of OTS by Th50
;
  (a,b // c,d & a,b // c,d1) or (a,b // c,d & a,b // d1,c) or
 (a,b // d,c & a,b // c,d1) or (a,b // d,c & a,b // d1,c) by A1,Th51;
then d=d1 or d1,c // c,d or d,c // c,d1 or (b,a // c,d & b,a // c,d1)
by A2,Def14; then d=d1 or (c =d & c =d1) by A2,Def14;
hence thesis; end;

Lm45: a,b // a,b
proof consider c such that A1: a,b // a,c or a,b // c,a by Def14;
A2: now assume A3: a,b // c,a; then c,a // a,b by Def14; then c =a & a=b
 by Def14; hence a,b // a,b by A3; end;
   now assume A4: a,b // a,c;
 A5: now assume A6: a<>c; a,c // a,b by A4,Def14;
  hence a,b // a,b by A6,Def14; end;
    now assume a=c; then a,a // a,b by A4,Def14;
  hence a,b // a,b by Def14; end;
 hence a,b // a,b by A5; end; hence thesis by A1,A2; end;

Lm46: a',b' // b',a'
proof reconsider a=a',b=b' as Element of OTS by Th50;
  a,b // a,b by Lm45; hence thesis by Th51; end;

definition let IT be non empty AffinStruct;
 attr IT is TrapSpace-like means
:Def15: for a',b',c',d',p',q' being Element of IT holds
  a',b' // b',a' & (a',b' // c',d' & a',b' // c',q' implies a'=b' or d'=q') &
  (p'<>q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d') &
  (a',b' // c',d' implies c',d' // a',b') &
   (ex x' being Element of IT st a',b' // c',x');
end;

definition
 cluster strict TrapSpace-like (non empty AffinStruct);
  existence
   proof consider OTS being OrdTrapSpace; set TS=Lambda(OTS);
       for a',b',c',d',p',q' being Element of TS holds
  a',b' // b',a' & (a',b' // c',d' & a',b' // c',q' implies a'=b' or d'=q') &
  (p'<>q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d') &
  (a',b' // c',d' implies c',d' // a',b') &
   (ex x' being Element of TS st a',b' // c',x')
    by Lm41,Lm42,Lm43,Lm44,Lm46;
     then TS is TrapSpace-like by Def15;
    hence thesis;
   end;
end;

definition
  mode TrapSpace is TrapSpace-like (non empty AffinStruct);
end;

definition let OTS be OrdTrapSpace;
 cluster Lambda(OTS) -> TrapSpace-like;
correctness proof
   Lambda(OTS) is TrapSpace-like
  proof
  let a',b',c',d',p',q' be Element of Lambda(OTS);
  thus thesis by Lm41,Lm42,Lm43,Lm44,Lm46; end;
  hence thesis;
 end;
end;

definition let IT be non empty AffinStruct;
 attr IT is Regular means :Def16:
 for p,q,a,a1,b,b1,c,c1,d,d1 being Element of IT
  st p<>q & p,q // a,a1 & p,q // b,b1 &
   p,q // c,c1 & p,q // d,d1 & a,b // c,d holds a1,b1 // c1,d1;
end;

definition cluster strict Regular (non empty OrdTrapSpace);
 existence proof consider MOTS being MidOrdTrapSpace; set X=Af(MOTS);
A1:X = AffinStruct(#the carrier of MOTS, the CONGR of MOTS#) by Def10;
A2: now let a,b,c,d be Element of X,
         a',b',c',d' be Element of
  the carrier of MOTS such that A3: a=a' & b=b' & c =c' & d=d';
  A4: now assume a,b // c,d;
   then [[a,b],[c,d]] in the CONGR of MOTS by A1,ANALOAF:def 2;
hence a',b' // c',d' by A3,ANALOAF:def 2; end;
     now assume a',b' // c',d'; then [[a,b],[c,d]] in the CONGR of MOTS by A3,
ANALOAF:def 2;hence a,b // c,d by A1,ANALOAF:def 2; end;
 hence a,b // c,d iff a',b' // c',d' by A4; end;
   now let p,q,a,a1,b,b1,c,c1,d,d1 be Element of X such that
  A5: p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
  a,b // c,d;
 reconsider a'=a,b'=b,c'=c,d'=d,a1'=a1,b1'=b1,c1'=c1,d1'=d1,p'=p,q'=q as
  Element of MOTS by A1;
     p'<>q' & p',q' // a',a1' & p',q' // b',b1' & p',q' // c',c1' &
   p',q' // d',d1' & a',b' // c',d' by A2,A5; then a1',b1' // c1',d1'
   by Def13; hence a1,b1 // c1,d1 by A2; end;
   then X is Regular by Def16;
  hence thesis;
 end;
end;

definition let MOS be MidOrdTrapSpace;
 cluster Af(MOS) -> Regular;
correctness proof set X=Af(MOS);
  now let p,q,a,a1,b,b1,c,c1,d,d1 be Element of X;
assume A1: p<>q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 &
 a,b // c,d;
A2:X = AffinStruct(#the carrier of MOS, the CONGR of MOS#) by Def10;
A3: now let a,b,c,d be Element of X, a',b',c',d' be Element of
  the carrier of MOS such that A4: a=a' & b=b' & c =c' & d=d';
  A5: now assume a,b // c,d;
   then [[a,b],[c,d]] in the CONGR of MOS by A2,ANALOAF:def 2;
hence a',b' // c',d' by A4,ANALOAF:def 2; end;
     now assume a',b' // c',d'; then [[a,b],[c,d]] in the CONGR of MOS by A4,
ANALOAF:def 2;hence a,b // c,d by A2,ANALOAF:def 2; end;
 hence a,b // c,d iff a',b' // c',d' by A5; end;
 reconsider a'=a,b'=b,c'=c,d'=d,a1'=a1,b1'=b1,c1'=c1,d1'=d1,p'=p,q'=q as
  Element of MOS by A2;
   p'<>q' & p',q' // a',a1' & p',q' // b',b1' & p',q' // c',c1' &
 p',q' // d',d1' &
 a',b' // c',d' by A1,A3; then a1',b1' // c1',d1' by Def13;
 hence a1,b1 // c1,d1 by A3; end;
  hence thesis by Def16;
 end; end;

Back to top