:: ANALORT semantic presentation

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) )
proof
let V be RealLinearSpace; ::_thesis: 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) )
let v1, x, y, v2 be VECTOR of V; ::_thesis: 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) )
let b1, b2, c1, c2 be Real; ::_thesis: ( v1 = (b1 * x) + (b2 * y) & v2 = (c1 * x) + (c2 * y) implies ( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) ) )
assume that
A1: v1 = (b1 * x) + (b2 * y) and
A2: v2 = (c1 * x) + (c2 * y) ; ::_thesis: ( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) )
thus v1 + v2 = (((b1 * x) + (b2 * y)) + (c1 * x)) + (c2 * y) by A1, A2, RLVECT_1:def_3
.= (((b1 * x) + (c1 * x)) + (b2 * y)) + (c2 * y) by RLVECT_1:def_3
.= (((b1 + c1) * x) + (b2 * y)) + (c2 * y) by RLVECT_1:def_6
.= ((b1 + c1) * x) + ((b2 * y) + (c2 * y)) by RLVECT_1:def_3
.= ((b1 + c1) * x) + ((b2 + c2) * y) by RLVECT_1:def_6 ; ::_thesis: v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y)
thus v1 - v2 = ((b1 * x) + (b2 * y)) + ((- (c1 * x)) + (- (c2 * y))) by A1, A2, RLVECT_1:31
.= ((b1 * x) + (b2 * y)) + ((c1 * (- x)) + (- (c2 * y))) by RLVECT_1:25
.= ((b1 * x) + (b2 * y)) + ((c1 * (- x)) + (c2 * (- y))) by RLVECT_1:25
.= ((b1 * x) + (b2 * y)) + (((- c1) * x) + (c2 * (- y))) by RLVECT_1:24
.= ((b1 * x) + (b2 * y)) + (((- c1) * x) + ((- c2) * y)) by RLVECT_1:24
.= (((b1 * x) + (b2 * y)) + ((- c1) * x)) + ((- c2) * y) by RLVECT_1:def_3
.= (((b1 * x) + ((- c1) * x)) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def_3
.= (((b1 + (- c1)) * x) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def_6
.= ((b1 + (- c1)) * x) + ((b2 * y) + ((- c2) * y)) by RLVECT_1:def_3
.= ((b1 - c1) * x) + ((b2 + (- c2)) * y) by RLVECT_1:def_6
.= ((b1 - c1) * x) + ((b2 - c2) * y) ; ::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: 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)
let v, x, y be VECTOR of V; ::_thesis: for b1, b2, a being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
let b1, b2, a be Real; ::_thesis: ( v = (b1 * x) + (b2 * y) implies a * v = ((a * b1) * x) + ((a * b2) * y) )
assume  v = (b1 * x) + (b2 * y) ; ::_thesis: a * v = ((a * b1) * x) + ((a * b2) * y)
hence a * v = (a * (b1 * x)) + (a * (b2 * y)) by RLVECT_1:def_5
.= ((a * b1) * x) + (a * (b2 * y)) by RLVECT_1:def_7
.= ((a * b1) * x) + ((a * b2) * y) by RLVECT_1:def_7 ;
::_thesis: verum
end;

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 )
proof
let V be RealLinearSpace; ::_thesis: 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 )
let x, y be VECTOR of V; ::_thesis: for a1, a2, b1, b2 being Real st Gen x,y & (a1 * x) + (a2 * y) = (b1 * x) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
let a1, a2, b1, b2 be Real; ::_thesis: ( Gen x,y & (a1 * x) + (a2 * y) = (b1 * x) + (b2 * y) implies ( a1 = b1 & a2 = b2 ) )
assume that
A1: Gen x,y and
A2: (a1 * x) + (a2 * y) = (b1 * x) + (b2 * y) ; ::_thesis: ( a1 = b1 & a2 = b2 )
A3: 0. V = ((a1 * x) + (a2 * y)) - ((b1 * x) + (b2 * y)) by A2, RLVECT_1:15
.= ((a1 - b1) * x) + ((a2 - b2) * y) by Lm1 ;
then A4: (- b1) + a1 = 0 by A1, ANALMETR:def_1;
 (- b2) + a2 = 0 by A1, A3, ANALMETR:def_1;
hence  ( a1 = b1 & a2 = b2 ) by A4; ::_thesis: verum
end;

Lm4:  for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
( x <> 0. V & y <> 0. V )
proof
let V be RealLinearSpace; ::_thesis: for x, y being VECTOR of V st Gen x,y holds
( x <> 0. V & y <> 0. V )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies ( x <> 0. V & y <> 0. V ) )
assume A1: Gen x,y ; ::_thesis: ( x <> 0. V & y <> 0. V )
A2: x <> 0. V
proof
assume A3: x = 0. V ; ::_thesis: contradiction
consider a, b being Real such that
A4: a = 1 and
A5: b = 0 ;
(a * x) + (b * y) = (0. V) + (0 * y) by A3, A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A1, A4, ANALMETR:def_1; ::_thesis: verum
end;
 y <> 0. V
proof
assume A6: y = 0. V ; ::_thesis: contradiction
consider a, b being Real such that
A7: a = 0 and
A8: b = 1 ;
(a * x) + (b * y) = (0. V) + (1 * (0. V)) by A6, A7, A8, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A1, A8, ANALMETR:def_1; ::_thesis: verum
end;
hence  ( x <> 0. V & y <> 0. V ) by A2; ::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: for x, y, u being VECTOR of V st Gen x,y holds
u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)
let x, y, u be VECTOR of V; ::_thesis: ( Gen x,y implies u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y) )
assume A1: Gen x,y ; ::_thesis: u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)
then  ex b being Real st u = ((pr1 (x,y,u)) * x) + (b * y) by GEOMTRAP:def_4;
hence  u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y) by A1, GEOMTRAP:def_5; ::_thesis: verum
end;

Lm6:  for V being RealLinearSpace
for x, y, u being VECTOR of V
for k1, k2 being Real st Gen x,y & u = (k1 * x) + (k2 * y) holds
( k1 = pr1 (x,y,u) & k2 = pr2 (x,y,u) )
proof
let V be RealLinearSpace; ::_thesis: for x, y, u being VECTOR of V
for k1, k2 being Real st Gen x,y & u = (k1 * x) + (k2 * y) holds
( k1 = pr1 (x,y,u) & k2 = pr2 (x,y,u) )
let x, y, u be VECTOR of V; ::_thesis: for k1, k2 being Real st Gen x,y & u = (k1 * x) + (k2 * y) holds
( k1 = pr1 (x,y,u) & k2 = pr2 (x,y,u) )
let k1, k2 be Real; ::_thesis: ( Gen x,y & u = (k1 * x) + (k2 * y) implies ( k1 = pr1 (x,y,u) & k2 = pr2 (x,y,u) ) )
assume that
A1: Gen x,y and
A2: u = (k1 * x) + (k2 * y) ; ::_thesis: ( k1 = pr1 (x,y,u) & k2 = pr2 (x,y,u) )
 u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y) by A1, Lm5;
hence  ( k1 = pr1 (x,y,u) & k2 = pr2 (x,y,u) ) by A1, A2, Lm3; ::_thesis: verum
end;

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)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
proof
let V be RealLinearSpace; ::_thesis: 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)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
let x, y, u, v be VECTOR of V; ::_thesis: for a being Real st Gen x,y holds
( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
let a be Real; ::_thesis: ( Gen x,y implies ( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) ) )
assume A1: Gen x,y ; ::_thesis: ( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) & pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
set p1u = pr1 (x,y,u);
set p2u = pr2 (x,y,u);
set p1v = pr1 (x,y,v);
set p2v = pr2 (x,y,v);
A2: u = ((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y) by A1, Lm5;
A3: v = ((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y) by A1, Lm5;
then u + v = ((((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)) + ((pr1 (x,y,v)) * x)) + ((pr2 (x,y,v)) * y) by A2, RLVECT_1:def_3
.= ((((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + ((pr2 (x,y,u)) * y)) + ((pr2 (x,y,v)) * y) by RLVECT_1:def_3
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (((pr2 (x,y,u)) * y) + ((pr2 (x,y,v)) * y)) by RLVECT_1:def_3
.= (((pr1 (x,y,u)) + (pr1 (x,y,v))) * x) + (((pr2 (x,y,u)) * y) + ((pr2 (x,y,v)) * y)) by RLVECT_1:def_6
.= (((pr1 (x,y,u)) + (pr1 (x,y,v))) * x) + (((pr2 (x,y,u)) + (pr2 (x,y,v))) * y) by RLVECT_1:def_6 ;
hence  ( pr1 (x,y,(u + v)) = (pr1 (x,y,u)) + (pr1 (x,y,v)) & pr2 (x,y,(u + v)) = (pr2 (x,y,u)) + (pr2 (x,y,v)) ) by A1, Lm6; ::_thesis: ( pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) & pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
 u - v = (((pr1 (x,y,u)) - (pr1 (x,y,v))) * x) + (((pr2 (x,y,u)) - (pr2 (x,y,v))) * y) by A2, A3, Lm1;
hence  ( pr1 (x,y,(u - v)) = (pr1 (x,y,u)) - (pr1 (x,y,v)) & pr2 (x,y,(u - v)) = (pr2 (x,y,u)) - (pr2 (x,y,v)) ) by A1, Lm6; ::_thesis: ( pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) )
 a * u = ((a * (pr1 (x,y,u))) * x) + ((a * (pr2 (x,y,u))) * y) by A2, Lm2;
hence  ( pr1 (x,y,(a * u)) = a * (pr1 (x,y,u)) & pr2 (x,y,(a * u)) = a * (pr2 (x,y,u)) ) by A1, Lm6; ::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: 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))
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y implies Ortm (x,y,(u + v)) = (Ortm (x,y,u)) + (Ortm (x,y,v)) )
assume A1: Gen x,y ; ::_thesis: Ortm (x,y,(u + v)) = (Ortm (x,y,u)) + (Ortm (x,y,v))
hence  Ortm (x,y,(u + v)) = (((pr1 (x,y,u)) + (pr1 (x,y,v))) * x) + ((- (pr2 (x,y,(u + v)))) * y) by Lm7
.= (((pr1 (x,y,u)) + (pr1 (x,y,v))) * x) + ((- ((pr2 (x,y,u)) + (pr2 (x,y,v)))) * y) by A1, Lm7
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + ((- ((pr2 (x,y,u)) + (pr2 (x,y,v)))) * y) by RLVECT_1:def_6
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (((pr2 (x,y,u)) + (pr2 (x,y,v))) * (- y)) by RLVECT_1:24
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (- (((pr2 (x,y,u)) + (pr2 (x,y,v))) * y)) by RLVECT_1:25
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + (- (((pr2 (x,y,u)) * y) + ((pr2 (x,y,v)) * y))) by RLVECT_1:def_6
.= (((pr1 (x,y,u)) * x) + ((pr1 (x,y,v)) * x)) + ((- ((pr2 (x,y,u)) * y)) + (- ((pr2 (x,y,v)) * y))) by RLVECT_1:31
.= ((pr1 (x,y,u)) * x) + (((pr1 (x,y,v)) * x) + ((- ((pr2 (x,y,u)) * y)) + (- ((pr2 (x,y,v)) * y)))) by RLVECT_1:def_3
.= ((pr1 (x,y,u)) * x) + ((- ((pr2 (x,y,u)) * y)) + (((pr1 (x,y,v)) * x) + (- ((pr2 (x,y,v)) * y)))) by RLVECT_1:def_3
.= (((pr1 (x,y,u)) * x) + (- ((pr2 (x,y,u)) * y))) + (((pr1 (x,y,v)) * x) + (- ((pr2 (x,y,v)) * y))) by RLVECT_1:def_3
.= (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y))) + (((pr1 (x,y,v)) * x) + (- ((pr2 (x,y,v)) * y))) by RLVECT_1:25
.= (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y))) + (((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * (- y))) by RLVECT_1:25
.= (((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y)) + (((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * (- y))) by RLVECT_1:24
.= (Ortm (x,y,u)) + (Ortm (x,y,v)) by RLVECT_1:24 ;
::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: 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))
let x, y, u be VECTOR of V; ::_thesis: for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
let n be Real; ::_thesis: ( Gen x,y implies Ortm (x,y,(n * u)) = n * (Ortm (x,y,u)) )
assume A1: Gen x,y ; ::_thesis: Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
hence  Ortm (x,y,(n * u)) = ((n * (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,(n * u)))) * y) by Lm7
.= ((n * (pr1 (x,y,u))) * x) + ((- (n * (pr2 (x,y,u)))) * y) by A1, Lm7
.= ((n * (pr1 (x,y,u))) * x) + ((n * (pr2 (x,y,u))) * (- y)) by RLVECT_1:24
.= ((n * (pr1 (x,y,u))) * x) + (- ((n * (pr2 (x,y,u))) * y)) by RLVECT_1:25
.= ((n * (pr1 (x,y,u))) * x) + (- (n * ((pr2 (x,y,u)) * y))) by RLVECT_1:def_7
.= ((n * (pr1 (x,y,u))) * x) + (n * (- ((pr2 (x,y,u)) * y))) by RLVECT_1:25
.= (n * ((pr1 (x,y,u)) * x)) + (n * (- ((pr2 (x,y,u)) * y))) by RLVECT_1:def_7
.= n * (((pr1 (x,y,u)) * x) + (- ((pr2 (x,y,u)) * y))) by RLVECT_1:def_5
.= n * (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y))) by RLVECT_1:25
.= n * (Ortm (x,y,u)) by RLVECT_1:24 ;
::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for x, y being VECTOR of V st Gen x,y holds
Ortm (x,y,(0. V)) = 0. V
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies Ortm (x,y,(0. V)) = 0. V )
assume A1: Gen x,y ; ::_thesis: Ortm (x,y,(0. V)) = 0. V
set u = the VECTOR of V;
thus  Ortm (x,y,(0. V)) = Ortm (x,y,(0 * the VECTOR of V)) by RLVECT_1:10
.= 0 * (Ortm (x,y, the VECTOR of V)) by A1, Th2
.= 0. V by RLVECT_1:10 ; ::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: for x, y, u being VECTOR of V st Gen x,y holds
Ortm (x,y,(- u)) = - (Ortm (x,y,u))
let x, y, u be VECTOR of V; ::_thesis: ( Gen x,y implies Ortm (x,y,(- u)) = - (Ortm (x,y,u)) )
assume A1: Gen x,y ; ::_thesis: Ortm (x,y,(- u)) = - (Ortm (x,y,u))
then A2: - u = - (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)) by Lm5
.= (- ((pr1 (x,y,u)) * x)) + (- ((pr2 (x,y,u)) * y)) by RLVECT_1:31
.= ((pr1 (x,y,u)) * (- x)) + (- ((pr2 (x,y,u)) * y)) by RLVECT_1:25
.= ((- (pr1 (x,y,u))) * x) + (- ((pr2 (x,y,u)) * y)) by RLVECT_1:24
.= ((- (pr1 (x,y,u))) * x) + ((pr2 (x,y,u)) * (- y)) by RLVECT_1:25
.= ((- (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,u))) * y) by RLVECT_1:24 ;
hence  Ortm (x,y,(- u)) = ((- (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,(- u)))) * y) by A1, Lm6
.= ((- (pr1 (x,y,u))) * x) + ((- (- (pr2 (x,y,u)))) * y) by A1, A2, Lm6
.= ((pr1 (x,y,u)) * (- x)) + ((- (- (pr2 (x,y,u)))) * y) by RLVECT_1:24
.= (- ((pr1 (x,y,u)) * x)) + ((- (- (pr2 (x,y,u)))) * y) by RLVECT_1:25
.= (- ((pr1 (x,y,u)) * x)) + ((- (pr2 (x,y,u))) * (- y)) by RLVECT_1:24
.= (- ((pr1 (x,y,u)) * x)) + (- ((- (pr2 (x,y,u))) * y)) by RLVECT_1:25
.= - (Ortm (x,y,u)) by RLVECT_1:31 ;
::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: 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))
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y implies Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v)) )
assume A1: Gen x,y ; ::_thesis: Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v))
hence  Ortm (x,y,(u - v)) = (Ortm (x,y,u)) + (Ortm (x,y,(- v))) by Th1
.= (Ortm (x,y,u)) - (Ortm (x,y,v)) by A1, Th4 ;
::_thesis: verum
end;

theorem Th6: :: ANALORT:6
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) holds
u = v
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v being VECTOR of V st Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) holds
u = v
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) implies u = v )
assume that
A1: Gen x,y and
A2: Ortm (x,y,u) = Ortm (x,y,v) ; ::_thesis: u = v
 (((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y)) - (((pr1 (x,y,v)) * x) + ((- (pr2 (x,y,v))) * y)) = 0. V by A2, RLVECT_1:15;
then  ((((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y)) - ((pr1 (x,y,v)) * x)) - ((- (pr2 (x,y,v))) * y) = 0. V by RLVECT_1:27;
then  ((((pr1 (x,y,u)) * x) + (- ((pr1 (x,y,v)) * x))) + ((- (pr2 (x,y,u))) * y)) - ((- (pr2 (x,y,v))) * y) = 0. V by RLVECT_1:def_3;
then  (((pr1 (x,y,u)) * x) - ((pr1 (x,y,v)) * x)) + (((- (pr2 (x,y,u))) * y) - ((- (pr2 (x,y,v))) * y)) = 0. V by RLVECT_1:def_3;
then  (((pr1 (x,y,u)) - (pr1 (x,y,v))) * x) + (((- (pr2 (x,y,u))) * y) - ((- (pr2 (x,y,v))) * y)) = 0. V by RLVECT_1:35;
then A3: (((pr1 (x,y,u)) - (pr1 (x,y,v))) * x) + (((- (pr2 (x,y,u))) - (- (pr2 (x,y,v)))) * y) = 0. V by RLVECT_1:35;
then A4: (pr1 (x,y,u)) - (pr1 (x,y,v)) = 0 by A1, ANALMETR:def_1;
 (- (pr2 (x,y,u))) - (- (pr2 (x,y,v))) = 0 by A1, A3, ANALMETR:def_1;
hence u = ((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y) by A1, A4, Lm5
.= v by A1, Lm5 ;
::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for x, y, u being VECTOR of V st Gen x,y holds
Ortm (x,y,(Ortm (x,y,u))) = u
let x, y, u be VECTOR of V; ::_thesis: ( Gen x,y implies Ortm (x,y,(Ortm (x,y,u))) = u )
assume A1: Gen x,y ; ::_thesis: Ortm (x,y,(Ortm (x,y,u))) = u
hence  Ortm (x,y,(Ortm (x,y,u))) = ((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,(((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y))))) * y) by GEOMTRAP:def_4
.= ((pr1 (x,y,u)) * x) + ((- (- (pr2 (x,y,u)))) * y) by A1, GEOMTRAP:def_5
.= u by A1, Lm5 ;
::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: 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)
let x, y, u be VECTOR of V; ::_thesis: ( Gen x,y implies ex v being VECTOR of V st u = Ortm (x,y,v) )
assume A1: Gen x,y ; ::_thesis: ex v being VECTOR of V st u = Ortm (x,y,v)
take  Ortm (x,y,u) ; ::_thesis: u = Ortm (x,y,(Ortm (x,y,u)))
thus  u = Ortm (x,y,(Ortm (x,y,u))) by A1, Th7; ::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: for x, y, v being VECTOR of V st Gen x,y holds
Orte (x,y,(- v)) = - (Orte (x,y,v))
let x, y, v be VECTOR of V; ::_thesis: ( Gen x,y implies Orte (x,y,(- v)) = - (Orte (x,y,v)) )
assume A1: Gen x,y ; ::_thesis: Orte (x,y,(- v)) = - (Orte (x,y,v))
then A2: - v = - (((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y)) by Lm5
.= (- ((pr1 (x,y,v)) * x)) + (- ((pr2 (x,y,v)) * y)) by RLVECT_1:31
.= ((pr1 (x,y,v)) * (- x)) + (- ((pr2 (x,y,v)) * y)) by RLVECT_1:25
.= ((- (pr1 (x,y,v))) * x) + (- ((pr2 (x,y,v)) * y)) by RLVECT_1:24
.= ((- (pr1 (x,y,v))) * x) + ((pr2 (x,y,v)) * (- y)) by RLVECT_1:25
.= ((- (pr1 (x,y,v))) * x) + ((- (pr2 (x,y,v))) * y) by RLVECT_1:24 ;
hence  Orte (x,y,(- v)) = ((- (pr2 (x,y,v))) * x) + ((- (pr1 (x,y,(- v)))) * y) by A1, Lm6
.= ((- (pr2 (x,y,v))) * x) + ((- (- (pr1 (x,y,v)))) * y) by A1, A2, Lm6
.= ((pr2 (x,y,v)) * (- x)) + ((- (- (pr1 (x,y,v)))) * y) by RLVECT_1:24
.= (- ((pr2 (x,y,v)) * x)) + ((- (- (pr1 (x,y,v)))) * y) by RLVECT_1:25
.= (- ((pr2 (x,y,v)) * x)) + ((- (pr1 (x,y,v))) * (- y)) by RLVECT_1:24
.= (- ((pr2 (x,y,v)) * x)) + (- ((- (pr1 (x,y,v))) * y)) by RLVECT_1:25
.= - (Orte (x,y,v)) by RLVECT_1:31 ;
::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: 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))
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y implies Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v)) )
assume A1: Gen x,y ; ::_thesis: Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v))
hence  Orte (x,y,(u + v)) = ((pr2 (x,y,(u + v))) * x) + ((- ((pr1 (x,y,u)) + (pr1 (x,y,v)))) * y) by Lm7
.= (((pr2 (x,y,u)) + (pr2 (x,y,v))) * x) + ((- ((pr1 (x,y,u)) + (pr1 (x,y,v)))) * y) by A1, Lm7
.= (((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + ((- ((pr1 (x,y,u)) + (pr1 (x,y,v)))) * y) by RLVECT_1:def_6
.= (((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + (((pr1 (x,y,u)) + (pr1 (x,y,v))) * (- y)) by RLVECT_1:24
.= (((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + (- (((pr1 (x,y,u)) + (pr1 (x,y,v))) * y)) by RLVECT_1:25
.= (((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + (- (((pr1 (x,y,u)) * y) + ((pr1 (x,y,v)) * y))) by RLVECT_1:def_6
.= (((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + ((- ((pr1 (x,y,u)) * y)) + (- ((pr1 (x,y,v)) * y))) by RLVECT_1:31
.= ((pr2 (x,y,u)) * x) + (((pr2 (x,y,v)) * x) + ((- ((pr1 (x,y,u)) * y)) + (- ((pr1 (x,y,v)) * y)))) by RLVECT_1:def_3
.= ((pr2 (x,y,u)) * x) + ((- ((pr1 (x,y,u)) * y)) + (((pr2 (x,y,v)) * x) + (- ((pr1 (x,y,v)) * y)))) by RLVECT_1:def_3
.= (((pr2 (x,y,u)) * x) + (- ((pr1 (x,y,u)) * y))) + (((pr2 (x,y,v)) * x) + (- ((pr1 (x,y,v)) * y))) by RLVECT_1:def_3
.= (((pr2 (x,y,u)) * x) + ((pr1 (x,y,u)) * (- y))) + (((pr2 (x,y,v)) * x) + (- ((pr1 (x,y,v)) * y))) by RLVECT_1:25
.= (((pr2 (x,y,u)) * x) + ((pr1 (x,y,u)) * (- y))) + (((pr2 (x,y,v)) * x) + ((pr1 (x,y,v)) * (- y))) by RLVECT_1:25
.= (((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y)) + (((pr2 (x,y,v)) * x) + ((pr1 (x,y,v)) * (- y))) by RLVECT_1:24
.= (Orte (x,y,u)) + (Orte (x,y,v)) by RLVECT_1:24 ;
::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: 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))
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y implies Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v)) )
assume A1: Gen x,y ; ::_thesis: Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v))
hence  Orte (x,y,(u - v)) = (Orte (x,y,u)) + (Orte (x,y,(- v))) by Th10
.= (Orte (x,y,u)) - (Orte (x,y,v)) by A1, Th9 ;
::_thesis: verum
end;

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))
proof
let V be RealLinearSpace; ::_thesis: 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))
let x, y, u be VECTOR of V; ::_thesis: for n being Real st Gen x,y holds
Orte (x,y,(n * u)) = n * (Orte (x,y,u))
let n be Real; ::_thesis: ( Gen x,y implies Orte (x,y,(n * u)) = n * (Orte (x,y,u)) )
assume A1: Gen x,y ; ::_thesis: Orte (x,y,(n * u)) = n * (Orte (x,y,u))
hence  Orte (x,y,(n * u)) = ((n * (pr2 (x,y,u))) * x) + ((- (pr1 (x,y,(n * u)))) * y) by Lm7
.= ((n * (pr2 (x,y,u))) * x) + ((- (n * (pr1 (x,y,u)))) * y) by A1, Lm7
.= ((n * (pr2 (x,y,u))) * x) + ((n * (pr1 (x,y,u))) * (- y)) by RLVECT_1:24
.= ((n * (pr2 (x,y,u))) * x) + (- ((n * (pr1 (x,y,u))) * y)) by RLVECT_1:25
.= ((n * (pr2 (x,y,u))) * x) + (- (n * ((pr1 (x,y,u)) * y))) by RLVECT_1:def_7
.= ((n * (pr2 (x,y,u))) * x) + (n * (- ((pr1 (x,y,u)) * y))) by RLVECT_1:25
.= (n * ((pr2 (x,y,u)) * x)) + (n * (- ((pr1 (x,y,u)) * y))) by RLVECT_1:def_7
.= n * (((pr2 (x,y,u)) * x) + (- ((pr1 (x,y,u)) * y))) by RLVECT_1:def_5
.= n * (((pr2 (x,y,u)) * x) + ((pr1 (x,y,u)) * (- y))) by RLVECT_1:25
.= n * (Orte (x,y,u)) by RLVECT_1:24 ;
::_thesis: verum
end;

theorem Th13: :: ANALORT:13
for V being RealLinearSpace
for x, y, u, v being VECTOR of V st Gen x,y & Orte (x,y,u) = Orte (x,y,v) holds
u = v
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v being VECTOR of V st Gen x,y & Orte (x,y,u) = Orte (x,y,v) holds
u = v
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y & Orte (x,y,u) = Orte (x,y,v) implies u = v )
assume that
A1: Gen x,y and
A2: Orte (x,y,u) = Orte (x,y,v) ; ::_thesis: u = v
 (((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y)) - (((pr2 (x,y,v)) * x) + ((- (pr1 (x,y,v))) * y)) = 0. V by A2, RLVECT_1:15;
then  ((((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y)) - ((pr2 (x,y,v)) * x)) - ((- (pr1 (x,y,v))) * y) = 0. V by RLVECT_1:27;
then  ((((pr2 (x,y,u)) * x) + (- ((pr2 (x,y,v)) * x))) + ((- (pr1 (x,y,u))) * y)) - ((- (pr1 (x,y,v))) * y) = 0. V by RLVECT_1:def_3;
then  (((pr2 (x,y,u)) * x) - ((pr2 (x,y,v)) * x)) + (((- (pr1 (x,y,u))) * y) - ((- (pr1 (x,y,v))) * y)) = 0. V by RLVECT_1:def_3;
then  (((pr2 (x,y,u)) - (pr2 (x,y,v))) * x) + (((- (pr1 (x,y,u))) * y) - ((- (pr1 (x,y,v))) * y)) = 0. V by RLVECT_1:35;
then A3: (((pr2 (x,y,u)) - (pr2 (x,y,v))) * x) + (((- (pr1 (x,y,u))) - (- (pr1 (x,y,v)))) * y) = 0. V by RLVECT_1:35;
then A4: (pr2 (x,y,u)) - (pr2 (x,y,v)) = 0 by A1, ANALMETR:def_1;
 (- (pr1 (x,y,u))) - (- (pr1 (x,y,v))) = 0 by A1, A3, ANALMETR:def_1;
hence u = ((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y) by A1, A4, Lm5
.= v by A1, Lm5 ;
::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for x, y, u being VECTOR of V st Gen x,y holds
Orte (x,y,(Orte (x,y,u))) = - u
let x, y, u be VECTOR of V; ::_thesis: ( Gen x,y implies Orte (x,y,(Orte (x,y,u))) = - u )
assume A1: Gen x,y ; ::_thesis: Orte (x,y,(Orte (x,y,u))) = - u
hence  Orte (x,y,(Orte (x,y,u))) = ((- (pr1 (x,y,u))) * x) + ((- (pr1 (x,y,(((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y))))) * y) by GEOMTRAP:def_5
.= ((- (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,u))) * y) by A1, GEOMTRAP:def_4
.= ((pr1 (x,y,u)) * (- x)) + ((- (pr2 (x,y,u))) * y) by RLVECT_1:24
.= (- ((pr1 (x,y,u)) * x)) + ((- (pr2 (x,y,u))) * y) by RLVECT_1:25
.= (- ((pr1 (x,y,u)) * x)) + ((pr2 (x,y,u)) * (- y)) by RLVECT_1:24
.= (- ((pr1 (x,y,u)) * x)) + (- ((pr2 (x,y,u)) * y)) by RLVECT_1:25
.= - (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)) by RLVECT_1:31
.= - u by A1, Lm5 ;
::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: 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
let x, y, u be VECTOR of V; ::_thesis: ( Gen x,y implies ex v being VECTOR of V st Orte (x,y,v) = u )
assume A1: Gen x,y ; ::_thesis: ex v being VECTOR of V st Orte (x,y,v) = u
take v = - (Orte (x,y,u)); ::_thesis: Orte (x,y,v) = u
thus  Orte (x,y,v) = - (Orte (x,y,(Orte (x,y,u)))) by A1, Th9
.= - (- u) by A1, Th14
.= u by RLVECT_1:17 ; ::_thesis: verum
end;

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 & u,v // u1,v1 holds
Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y & u,v // u1,v1 implies Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1) )
assume A1: Gen x,y ; ::_thesis: ( not u,v // u1,v1 or Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1) )
assume A2: u,v // u1,v1 ; ::_thesis: Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
now__::_thesis:_(_u_<>_v_&_u1_<>_v1_implies_Orte_(x,y,u),_Orte_(x,y,v)_//_Orte_(x,y,u1),_Orte_(x,y,v1)_)
assume that
A3: u <> v and
A4: u1 <> v1 ; ::_thesis: Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
consider a, b being Real such that
A5: 0 < a and
A6: 0 < b and
A7: a * (v - u) = b * (v1 - u1) by A2, A3, A4, ANALOAF:def_1;
a * ((Orte (x,y,v)) - (Orte (x,y,u))) = a * (Orte (x,y,(v - u))) by A1, Th11
.= Orte (x,y,(b * (v1 - u1))) by A1, A7, Th12
.= b * (Orte (x,y,(v1 - u1))) by A1, Th12
.= b * ((Orte (x,y,v1)) - (Orte (x,y,u1))) by A1, Th11 ;
hence  Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1) by A5, A6, ANALOAF:def_1; ::_thesis: verum
end;
hence  Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1) by ANALOAF:9; ::_thesis: verum
end;

theorem Th17: :: ANALORT:17
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y & u,v // u1,v1 implies Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) )
assume A1: Gen x,y ; ::_thesis: ( not u,v // u1,v1 or Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) )
assume A2: u,v // u1,v1 ; ::_thesis: Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
now__::_thesis:_(_u_<>_v_implies_Ortm_(x,y,u),_Ortm_(x,y,v)_//_Ortm_(x,y,u1),_Ortm_(x,y,v1)_)
assume A3: u <> v ; ::_thesis: Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
now__::_thesis:_(_u1_<>_v1_implies_Ortm_(x,y,u),_Ortm_(x,y,v)_//_Ortm_(x,y,u1),_Ortm_(x,y,v1)_)
assume  u1 <> v1 ; ::_thesis: Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
then consider a, b being Real such that
A4: 0 < a and
A5: 0 < b and
A6: a * (v - u) = b * (v1 - u1) by A2, A3, ANALOAF:def_1;
a * ((Ortm (x,y,v)) - (Ortm (x,y,u))) = a * (Ortm (x,y,(v - u))) by A1, Th5
.= Ortm (x,y,(b * (v1 - u1))) by A1, A6, Th2
.= b * (Ortm (x,y,(v1 - u1))) by A1, Th2
.= b * ((Ortm (x,y,v1)) - (Ortm (x,y,u1))) by A1, Th5 ;
hence  Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) by A4, A5, ANALOAF:def_1; ::_thesis: verum
end;
hence  Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) by ANALOAF:9; ::_thesis: verum
end;
hence  Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) by ANALOAF:9; ::_thesis: verum
end;

theorem Th18: :: ANALORT:18
for V being RealLinearSpace
for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y holds
v,v1,u1,u are_COrte_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y holds
v,v1,u1,u are_COrte_wrt x,y
let x, y, u, u1, v, v1 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y implies v,v1,u1,u are_COrte_wrt x,y )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrte_wrt x,y or v,v1,u1,u are_COrte_wrt x,y )
assume  u,u1,v,v1 are_COrte_wrt x,y ; ::_thesis: v,v1,u1,u are_COrte_wrt x,y
then  Orte (x,y,u), Orte (x,y,u1) // v,v1 by Def3;
then  v,v1 // Orte (x,y,u), Orte (x,y,u1) by ANALOAF:12;
then  Orte (x,y,v), Orte (x,y,v1) // Orte (x,y,(Orte (x,y,u))), Orte (x,y,(Orte (x,y,u1))) by A1, Th16;
then  Orte (x,y,v), Orte (x,y,v1) // - u, Orte (x,y,(Orte (x,y,u1))) by A1, Th14;
then  Orte (x,y,v), Orte (x,y,v1) // - u, - u1 by A1, Th14;
then A2: - u, - u1 // Orte (x,y,v), Orte (x,y,v1) by ANALOAF:12;
(- u1) - (- u) = u + (- u1) by RLVECT_1:17
.= u - u1 ;
then A3: - u, - u1 // u1,u by ANALOAF:15;
A4: now__::_thesis:_(_-_u_<>_-_u1_implies_v,v1,u1,u_are_COrte_wrt_x,y_)
assume  - u <> - u1 ; ::_thesis: v,v1,u1,u are_COrte_wrt x,y
then  Orte (x,y,v), Orte (x,y,v1) // u1,u by A2, A3, ANALOAF:11;
hence  v,v1,u1,u are_COrte_wrt x,y by Def3; ::_thesis: verum
end;
now__::_thesis:_(_-_u_=_-_u1_implies_v,v1,u1,u_are_COrte_wrt_x,y_)
assume  - u = - u1 ; ::_thesis: v,v1,u1,u are_COrte_wrt x,y
then u = - (- u1) by RLVECT_1:17
.= u1 by RLVECT_1:17 ;
then  Orte (x,y,v), Orte (x,y,v1) // u1,u by ANALOAF:9;
hence  v,v1,u1,u are_COrte_wrt x,y by Def3; ::_thesis: verum
end;
hence  v,v1,u1,u are_COrte_wrt x,y by A4; ::_thesis: verum
end;

theorem Th19: :: ANALORT:19
for V being RealLinearSpace
for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y holds
v,v1,u,u1 are_COrtm_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y holds
v,v1,u,u1 are_COrtm_wrt x,y
let x, y, u, u1, v, v1 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y implies v,v1,u,u1 are_COrtm_wrt x,y )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or v,v1,u,u1 are_COrtm_wrt x,y )
assume  u,u1,v,v1 are_COrtm_wrt x,y ; ::_thesis: v,v1,u,u1 are_COrtm_wrt x,y
then  Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by Def4;
then  v,v1 // Ortm (x,y,u), Ortm (x,y,u1) by ANALOAF:12;
then  Ortm (x,y,v), Ortm (x,y,v1) // Ortm (x,y,(Ortm (x,y,u))), Ortm (x,y,(Ortm (x,y,u1))) by A1, Th17;
then  Ortm (x,y,v), Ortm (x,y,v1) // u, Ortm (x,y,(Ortm (x,y,u1))) by A1, Th7;
then  Ortm (x,y,v), Ortm (x,y,v1) // u,u1 by A1, Th7;
hence  v,v1,u,u1 are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y
let u, v, w, x, y be VECTOR of V; ::_thesis: u,u,v,w are_COrte_wrt x,y
 Orte (x,y,u), Orte (x,y,u) // v,w by ANALOAF:9;
hence  u,u,v,w are_COrte_wrt x,y by Def3; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrtm_wrt x,y
let u, v, w, x, y be VECTOR of V; ::_thesis: u,u,v,w are_COrtm_wrt x,y
 Ortm (x,y,u), Ortm (x,y,u) // v,w by ANALOAF:9;
hence  u,u,v,w are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrte_wrt x,y
let u, v, w, x, y be VECTOR of V; ::_thesis: u,v,w,w are_COrte_wrt x,y
 Orte (x,y,u), Orte (x,y,v) // w,w by ANALOAF:9;
hence  u,v,w,w are_COrte_wrt x,y by Def3; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrtm_wrt x,y
let u, v, w, x, y be VECTOR of V; ::_thesis: u,v,w,w are_COrtm_wrt x,y
 Ortm (x,y,u), Ortm (x,y,v) // w,w by ANALOAF:9;
hence  u,v,w,w are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: 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
let x, y, u, v be VECTOR of V; ::_thesis: ( Gen x,y implies u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y )
assume A1: Gen x,y ; ::_thesis: u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y
set w = (Orte (x,y,v)) - (Orte (x,y,u));
A2: (Orte (x,y,v)) - (Orte (x,y,u)) = Orte (x,y,(v - u)) by A1, Th11
.= ((pr2 (x,y,(v - u))) * x) + ((- (pr1 (x,y,(v - u)))) * y) ;
PProJ (x,y,(v - u),((Orte (x,y,v)) - (Orte (x,y,u)))) = ((pr1 (x,y,(v - u))) * (pr1 (x,y,((Orte (x,y,v)) - (Orte (x,y,u)))))) + ((pr2 (x,y,(v - u))) * (pr2 (x,y,((Orte (x,y,v)) - (Orte (x,y,u)))))) by GEOMTRAP:def_6
.= ((pr1 (x,y,(v - u))) * (pr2 (x,y,(v - u)))) + ((pr2 (x,y,(v - u))) * (pr2 (x,y,((Orte (x,y,v)) - (Orte (x,y,u)))))) by A1, A2, Lm6
.= ((pr1 (x,y,(v - u))) * (pr2 (x,y,(v - u)))) + ((- (pr1 (x,y,(v - u)))) * (pr2 (x,y,(v - u)))) by A1, A2, Lm6
.= 0 ;
then  v - u,(Orte (x,y,v)) - (Orte (x,y,u)) are_Ort_wrt x,y by A1, GEOMTRAP:32;
hence  u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y by ANALMETR:def_3; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: 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
let u, v, x, y be VECTOR of V; ::_thesis: u,v, Orte (x,y,u), Orte (x,y,v) are_COrte_wrt x,y
 Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u), Orte (x,y,v) by ANALOAF:8;
hence  u,v, Orte (x,y,u), Orte (x,y,v) are_COrte_wrt x,y by Def3; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: 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
let u, v, x, y be VECTOR of V; ::_thesis: u,v, Ortm (x,y,u), Ortm (x,y,v) are_COrtm_wrt x,y
 Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u), Ortm (x,y,v) by ANALOAF:8;
hence  u,v, Ortm (x,y,u), Ortm (x,y,v) are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;

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 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
proof
let V be RealLinearSpace; ::_thesis: 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 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y implies ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) ) )
assume A1: Gen x,y ; ::_thesis: ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
A2: ( u,v // u1,v1 implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
proof
assume A3: u,v // u1,v1 ; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
A4: now__::_thesis:_(_u_=_v_&_u1_=_v1_implies_ex_u2_being_M2(_the_carrier_of_V)_ex_v2,_u2,_v2_being_VECTOR_of_V_st_
(_u2_<>_v2_&_u2,v2,u,v_are_COrte_wrt_x,y_&_u2,v2,u1,v1_are_COrte_wrt_x,y_)_)
assume that
A5: u = v and
A6: u1 = v1 ; ::_thesis: ex u2 being M2( the carrier of V) ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
take u2 = 0. V; ::_thesis: ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
take v2 = x; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
A7: Orte (x,y,u2), Orte (x,y,v2) // u,v by A5, ANALOAF:9;
 Orte (x,y,u2), Orte (x,y,v2) // u1,v1 by A6, ANALOAF:9;
then A8: u2,v2,u1,v1 are_COrte_wrt x,y by Def3;
A9: u2,v2,u,v are_COrte_wrt x,y by A7, Def3;
 u2 <> v2 by A1, Lm4;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A8, A9; ::_thesis: verum
end;
A10: now__::_thesis:_(_u_<>_v_implies_ex_u2,_v2_being_VECTOR_of_V_st_
(_u2_<>_v2_&_u2,v2,u,v_are_COrte_wrt_x,y_&_u2,v2,u1,v1_are_COrte_wrt_x,y_)_)
assume A11: u <> v ; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A12: Orte (x,y,u2) = u by A1, Th15;
consider v2 being VECTOR of V such that
A13: Orte (x,y,v2) = v by A1, Th15;
 Orte (x,y,u2), Orte (x,y,v2) // u,v by A12, A13, ANALOAF:8;
then A14: u2,v2,u,v are_COrte_wrt x,y by Def3;
 u2,v2,u1,v1 are_COrte_wrt x,y by A3, A12, A13, Def3;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A11, A12, A13, A14; ::_thesis: verum
end;
now__::_thesis:_(_u1_<>_v1_implies_ex_u2,_v2_being_VECTOR_of_V_st_
(_u2_<>_v2_&_u2,v2,u,v_are_COrte_wrt_x,y_&_u2,v2,u1,v1_are_COrte_wrt_x,y_)_)
assume A15: u1 <> v1 ; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A16: Orte (x,y,u2) = u1 by A1, Th15;
consider v2 being VECTOR of V such that
A17: Orte (x,y,v2) = v1 by A1, Th15;
 Orte (x,y,u2), Orte (x,y,v2) // u1,v1 by A16, A17, ANALOAF:8;
then A18: u2,v2,u1,v1 are_COrte_wrt x,y by Def3;
 Orte (x,y,u2), Orte (x,y,v2) // u,v by A3, A16, A17, ANALOAF:12;
then  u2,v2,u,v are_COrte_wrt x,y by Def3;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A15, A16, A17, A18; ::_thesis: verum
end;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A4, A10; ::_thesis: verum
end;
 ( ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) implies u,v // u1,v1 )
proof
given u2, v2 being VECTOR of V such that A19: u2 <> v2 and
A20: u2,v2,u,v are_COrte_wrt x,y and
A21: u2,v2,u1,v1 are_COrte_wrt x,y ; ::_thesis: u,v // u1,v1
A22: Orte (x,y,u2), Orte (x,y,v2) // u,v by A20, Def3;
 Orte (x,y,u2), Orte (x,y,v2) // u1,v1 by A21, Def3;
hence  u,v // u1,v1 by A1, A19, A22, Th13, ANALOAF:11; ::_thesis: verum
end;
hence  ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) ) by A2; ::_thesis: verum
end;

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 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
proof
let V be RealLinearSpace; ::_thesis: 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 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y implies ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) ) )
assume A1: Gen x,y ; ::_thesis: ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
A2: ( u,v // u1,v1 implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
proof
assume A3: u,v // u1,v1 ; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
A4: now__::_thesis:_(_u_=_v_&_u1_=_v1_implies_ex_u2_being_M2(_the_carrier_of_V)_ex_v2,_u2,_v2_being_VECTOR_of_V_st_
(_u2_<>_v2_&_u2,v2,u,v_are_COrtm_wrt_x,y_&_u2,v2,u1,v1_are_COrtm_wrt_x,y_)_)
assume that
A5: u = v and
A6: u1 = v1 ; ::_thesis: ex u2 being M2( the carrier of V) ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
take u2 = 0. V; ::_thesis: ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
take v2 = x; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
A7: Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A5, ANALOAF:9;
 Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by A6, ANALOAF:9;
then A8: u2,v2,u1,v1 are_COrtm_wrt x,y by Def4;
A9: u2,v2,u,v are_COrtm_wrt x,y by A7, Def4;
 u2 <> v2 by A1, Lm4;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) by A8, A9; ::_thesis: verum
end;
A10: now__::_thesis:_(_u_<>_v_implies_ex_u2,_v2_being_VECTOR_of_V_st_
(_u2_<>_v2_&_u2,v2,u,v_are_COrtm_wrt_x,y_&_u2,v2,u1,v1_are_COrtm_wrt_x,y_)_)
assume A11: u <> v ; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A12: Ortm (x,y,u2) = u by A1, Th8;
consider v2 being VECTOR of V such that
A13: Ortm (x,y,v2) = v by A1, Th8;
 Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A12, A13, ANALOAF:8;
then A14: u2,v2,u,v are_COrtm_wrt x,y by Def4;
 u2,v2,u1,v1 are_COrtm_wrt x,y by A3, A12, A13, Def4;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) by A11, A12, A13, A14; ::_thesis: verum
end;
now__::_thesis:_(_u1_<>_v1_implies_ex_u2,_v2_being_VECTOR_of_V_st_
(_u2_<>_v2_&_u2,v2,u,v_are_COrtm_wrt_x,y_&_u2,v2,u1,v1_are_COrtm_wrt_x,y_)_)
assume A15: u1 <> v1 ; ::_thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A16: Ortm (x,y,u2) = u1 by A1, Th8;
consider v2 being VECTOR of V such that
A17: Ortm (x,y,v2) = v1 by A1, Th8;
 Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by A16, A17, ANALOAF:8;
then A18: u2,v2,u1,v1 are_COrtm_wrt x,y by Def4;
 Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A3, A16, A17, ANALOAF:12;
then  u2,v2,u,v are_COrtm_wrt x,y by Def4;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) by A15, A16, A17, A18; ::_thesis: verum
end;
hence  ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) by A4, A10; ::_thesis: verum
end;
 ( ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) implies u,v // u1,v1 )
proof
given u2, v2 being VECTOR of V such that A19: u2 <> v2 and
A20: u2,v2,u,v are_COrtm_wrt x,y and
A21: u2,v2,u1,v1 are_COrtm_wrt x,y ; ::_thesis: u,v // u1,v1
A22: Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A20, Def4;
 Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by A21, Def4;
hence  u,v // u1,v1 by A1, A19, A22, Th6, ANALOAF:11; ::_thesis: verum
end;
hence  ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) ) by A2; ::_thesis: verum
end;

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 ) )
proof
let V be RealLinearSpace; ::_thesis: 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 ) )
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y implies ( 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 ) ) )
assume A1: Gen x,y ; ::_thesis: ( 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 ) )
A2: now__::_thesis:_(_u_=_v_implies_u,v,u1,v1_are_Ort_wrt_x,y_)
assume  u = v ; ::_thesis: u,v,u1,v1 are_Ort_wrt x,y
then  v - u = 0. V by RLVECT_1:15;
then  v - u,v1 - u1 are_Ort_wrt x,y by A1, ANALMETR:5;
hence  u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def_3; ::_thesis: verum
end;
now__::_thesis:_(_u_<>_v_implies_(_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_)_)_)
assume A3: u <> v ; ::_thesis: ( 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 ) )
set u2 = Orte (x,y,u);
set v2 = Orte (x,y,v);
A4: v - u <> 0. V by A3, RLVECT_1:21;
 u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y by A1, Th24;
then A5: v - u,(Orte (x,y,v)) - (Orte (x,y,u)) are_Ort_wrt x,y by ANALMETR:def_3;
A6: now__::_thesis:_(_not_u,v,u1,v1_are_Ort_wrt_x,y_or_u,v,u1,v1_are_COrte_wrt_x,y_or_u,v,v1,u1_are_COrte_wrt_x,y_)
assume  u,v,u1,v1 are_Ort_wrt x,y ; ::_thesis: ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y )
then  v - u,v1 - u1 are_Ort_wrt x,y by ANALMETR:def_3;
then  ex a, b being Real st
( a * ((Orte (x,y,v)) - (Orte (x,y,u))) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A1, A4, A5, ANALMETR:9;
then  ( Orte (x,y,u), Orte (x,y,v) // u1,v1 or Orte (x,y,u), Orte (x,y,v) // v1,u1 ) by ANALMETR:14;
hence  ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) by Def3; ::_thesis: verum
end;
now__::_thesis:_(_(_u,v,u1,v1_are_COrte_wrt_x,y_or_u,v,v1,u1_are_COrte_wrt_x,y_)_implies_u,v,u1,v1_are_Ort_wrt_x,y_)
assume  ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ; ::_thesis: u,v,u1,v1 are_Ort_wrt x,y
then  ( Orte (x,y,u), Orte (x,y,v) // u1,v1 or Orte (x,y,u), Orte (x,y,v) // v1,u1 ) by Def3;
then consider a, b being Real such that
A7: a * ((Orte (x,y,v)) - (Orte (x,y,u))) = b * (v1 - u1) and
A8: ( a <> 0 or b <> 0 ) by ANALMETR:14;
A9: now__::_thesis:_(_b_=_0_implies_u,v,u1,v1_are_Ort_wrt_x,y_)
assume A10: b = 0 ; ::_thesis: u,v,u1,v1 are_Ort_wrt x,y
then  0. V = a * ((Orte (x,y,v)) - (Orte (x,y,u))) by A7, RLVECT_1:10;
then  (Orte (x,y,v)) - (Orte (x,y,u)) = 0. V by A8, A10, RLVECT_1:11;
then  Orte (x,y,v) = Orte (x,y,u) by RLVECT_1:21;
then  u = v by A1, Th13;
then  v - u = 0. V by RLVECT_1:15;
then  v - u,v1 - u1 are_Ort_wrt x,y by A1, ANALMETR:5;
hence  u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def_3; ::_thesis: verum
end;
now__::_thesis:_(_b_<>_0_implies_u,v,u1,v1_are_Ort_wrt_x,y_)
assume A11: b <> 0 ; ::_thesis: u,v,u1,v1 are_Ort_wrt x,y
 ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) = (b ") * (b * (v1 - u1)) by A7, RLVECT_1:def_7;
then  ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) = ((b ") * b) * (v1 - u1) by RLVECT_1:def_7;
then  ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) = 1 * (v1 - u1) by A11, XCMPLX_0:def_7;
then  v1 - u1 = ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) by RLVECT_1:def_8;
then  v - u,v1 - u1 are_Ort_wrt x,y by A5, ANALMETR:7;
hence  u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def_3; ::_thesis: verum
end;
hence  u,v,u1,v1 are_Ort_wrt x,y by A9; ::_thesis: verum
end;
hence  ( 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 ) ) by A6; ::_thesis: verum
end;
hence  ( 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 ) ) by A2, Th20; ::_thesis: verum
end;

theorem :: ANALORT:30
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y & not u = v holds
u1 = v1
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y & not u = v holds
u1 = v1
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y & not u = v implies u1 = v1 )
assume A1: Gen x,y ; ::_thesis: ( not u,v,u1,v1 are_COrte_wrt x,y or not u,v,v1,u1 are_COrte_wrt x,y or u = v or u1 = v1 )
assume that
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,v1,u1 are_COrte_wrt x,y ; ::_thesis: ( u = v or u1 = v1 )
assume that
A4: u <> v and
A5: u1 <> v1 ; ::_thesis: contradiction
A6: Orte (x,y,u), Orte (x,y,v) // u1,v1 by A2, Def3;
A7: Orte (x,y,u), Orte (x,y,v) // v1,u1 by A3, Def3;
 Orte (x,y,u) <> Orte (x,y,v) by A1, A4, Th13;
hence  contradiction by A5, A6, A7, ANALOAF:10, ANALOAF:11; ::_thesis: verum
end;

theorem :: ANALORT:31
for V being RealLinearSpace
for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v holds
u1 = v1
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v holds
u1 = v1
let x, y, u, v, u1, v1 be VECTOR of V; ::_thesis: ( Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v implies u1 = v1 )
assume A1: Gen x,y ; ::_thesis: ( not u,v,u1,v1 are_COrtm_wrt x,y or not u,v,v1,u1 are_COrtm_wrt x,y or u = v or u1 = v1 )
assume that
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,v1,u1 are_COrtm_wrt x,y ; ::_thesis: ( u = v or u1 = v1 )
assume that
A4: u <> v and
A5: u1 <> v1 ; ::_thesis: contradiction
A6: Ortm (x,y,u), Ortm (x,y,v) // u1,v1 by A2, Def4;
A7: Ortm (x,y,u), Ortm (x,y,v) // v1,u1 by A3, Def4;
 Ortm (x,y,u) <> Ortm (x,y,v) by A1, A4, Th6;
hence  contradiction by A5, A6, A7, ANALOAF:10, ANALOAF:11; ::_thesis: verum
end;

theorem :: ANALORT:32
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y & not u,v,v1,w are_COrte_wrt x,y holds
u,v,w,v1 are_COrte_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y & not u,v,v1,w are_COrte_wrt x,y holds
u,v,w,v1 are_COrte_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; ::_thesis: ( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y & not u,v,v1,w are_COrte_wrt x,y implies u,v,w,v1 are_COrte_wrt x,y )
assume that
A1: Gen x,y and
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,u1,w are_COrte_wrt x,y ; ::_thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
A4: Orte (x,y,u), Orte (x,y,v) // u1,v1 by A2, Def3;
A5: Orte (x,y,u), Orte (x,y,v) // u1,w by A3, Def3;
now__::_thesis:_(_u_<>_v_&_not_u,v,v1,w_are_COrte_wrt_x,y_implies_u,v,w,v1_are_COrte_wrt_x,y_)
assume A6: u <> v ; ::_thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
now__::_thesis:_(_u1_<>_v1_&_u1_<>_w_&_not_u,v,v1,w_are_COrte_wrt_x,y_implies_u,v,w,v1_are_COrte_wrt_x,y_)
assume that
A7: u1 <> v1 and
A8: u1 <> w ; ::_thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
A9: u1,v1 // u1,w by A1, A4, A5, A6, Th13, ANALOAF:11;
A10: now__::_thesis:_(_u1,v1_//_v1,w_&_not_u,v,v1,w_are_COrte_wrt_x,y_implies_u,v,w,v1_are_COrte_wrt_x,y_)
assume A11: u1,v1 // v1,w ; ::_thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
 u1,v1 // Orte (x,y,u), Orte (x,y,v) by A4, ANALOAF:12;
then  Orte (x,y,u), Orte (x,y,v) // v1,w by A7, A11, ANALOAF:11;
hence  ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by Def3; ::_thesis: verum
end;
now__::_thesis:_(_u1,w_//_w,v1_&_not_u,v,v1,w_are_COrte_wrt_x,y_implies_u,v,w,v1_are_COrte_wrt_x,y_)
assume A12: u1,w // w,v1 ; ::_thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
 u1,w // Orte (x,y,u), Orte (x,y,v) by A5, ANALOAF:12;
then  Orte (x,y,u), Orte (x,y,v) // w,v1 by A8, A12, ANALOAF:11;
hence  ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by Def3; ::_thesis: verum
end;
hence  ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by A9, A10, ANALOAF:14; ::_thesis: verum
end;
hence  ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by A2, A3; ::_thesis: verum
end;
hence  ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by Th20; ::_thesis: verum
end;

theorem :: ANALORT:33
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y & not u,v,v1,w are_COrtm_wrt x,y holds
u,v,w,v1 are_COrtm_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y & not u,v,v1,w are_COrtm_wrt x,y holds
u,v,w,v1 are_COrtm_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; ::_thesis: ( Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y & not u,v,v1,w are_COrtm_wrt x,y implies u,v,w,v1 are_COrtm_wrt x,y )
assume that
A1: Gen x,y and
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,u1,w are_COrtm_wrt x,y ; ::_thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
A4: Ortm (x,y,u), Ortm (x,y,v) // u1,v1 by A2, Def4;
A5: Ortm (x,y,u), Ortm (x,y,v) // u1,w by A3, Def4;
A6: now__::_thesis:_(_u_<>_v_&_u1_<>_v1_&_not_u,v,v1,w_are_COrtm_wrt_x,y_implies_u,v,w,v1_are_COrtm_wrt_x,y_)
assume that
A7: u <> v and
A8: u1 <> v1 ; ::_thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
 u1,v1 // u1,w by A1, A4, A5, A7, Th6, ANALOAF:11;
then A9: ( u1,v1 // v1,w or u1,w // w,v1 ) by ANALOAF:14;
now__::_thesis:_(_u1_<>_w_&_not_u,v,v1,w_are_COrtm_wrt_x,y_implies_u,v,w,v1_are_COrtm_wrt_x,y_)
assume A10: u1 <> w ; ::_thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
A11: u1,v1 // Ortm (x,y,u), Ortm (x,y,v) by A4, ANALOAF:12;
 u1,w // Ortm (x,y,u), Ortm (x,y,v) by A5, ANALOAF:12;
then  ( Ortm (x,y,u), Ortm (x,y,v) // v1,w or Ortm (x,y,u), Ortm (x,y,v) // w,v1 ) by A8, A9, A10, A11, ANALOAF:11;
hence  ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by Def4; ::_thesis: verum
end;
hence  ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by A2; ::_thesis: verum
end;
now__::_thesis:_(_u_=_v_&_not_u,v,v1,w_are_COrtm_wrt_x,y_implies_u,v,w,v1_are_COrtm_wrt_x,y_)
assume  u = v ; ::_thesis: ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y )
then  ( Ortm (x,y,u), Ortm (x,y,v) // v1,w or Ortm (x,y,u), Ortm (x,y,v) // w,v1 ) by ANALOAF:9;
hence  ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by Def4; ::_thesis: verum
end;
hence  ( u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y ) by A3, A6; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: 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
let u, v, u1, v1, x, y be VECTOR of V; ::_thesis: ( u,v,u1,v1 are_COrte_wrt x,y implies v,u,v1,u1 are_COrte_wrt x,y )
assume  u,v,u1,v1 are_COrte_wrt x,y ; ::_thesis: v,u,v1,u1 are_COrte_wrt x,y
then  Orte (x,y,u), Orte (x,y,v) // u1,v1 by Def3;
then  Orte (x,y,v), Orte (x,y,u) // v1,u1 by ANALOAF:12;
hence  v,u,v1,u1 are_COrte_wrt x,y by Def3; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: 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
let u, v, u1, v1, x, y be VECTOR of V; ::_thesis: ( u,v,u1,v1 are_COrtm_wrt x,y implies v,u,v1,u1 are_COrtm_wrt x,y )
assume  u,v,u1,v1 are_COrtm_wrt x,y ; ::_thesis: v,u,v1,u1 are_COrtm_wrt x,y
then  Ortm (x,y,u), Ortm (x,y,v) // u1,v1 by Def4;
then  Ortm (x,y,v), Ortm (x,y,u) // v1,u1 by ANALOAF:12;
hence  v,u,v1,u1 are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;

theorem :: ANALORT:36
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y holds
u,v,u1,w are_COrte_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y holds
u,v,u1,w are_COrte_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; ::_thesis: ( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y implies u,v,u1,w are_COrte_wrt x,y )
assume A1: Gen x,y ; ::_thesis: ( not u,v,u1,v1 are_COrte_wrt x,y or not u,v,v1,w are_COrte_wrt x,y or u,v,u1,w are_COrte_wrt x,y )
assume that
A2: u,v,u1,v1 are_COrte_wrt x,y and
A3: u,v,v1,w are_COrte_wrt x,y ; ::_thesis: u,v,u1,w are_COrte_wrt x,y
A4: Orte (x,y,u), Orte (x,y,v) // u1,v1 by A2, Def3;
A5: Orte (x,y,u), Orte (x,y,v) // v1,w by A3, Def3;
A6: u1,v1 // Orte (x,y,u), Orte (x,y,v) by A4, ANALOAF:12;
A7: now__::_thesis:_(_u_<>_v_implies_u,v,u1,w_are_COrte_wrt_x,y_)
assume  u <> v ; ::_thesis: u,v,u1,w are_COrte_wrt x,y
then  u1,v1 // v1,w by A1, A4, A5, Th13, ANALOAF:11;
then A8: u1,v1 // u1,w by ANALOAF:13;
now__::_thesis:_(_u1_<>_v1_implies_u,v,u1,w_are_COrte_wrt_x,y_)
assume  u1 <> v1 ; ::_thesis: u,v,u1,w are_COrte_wrt x,y
then  Orte (x,y,u), Orte (x,y,v) // u1,w by A6, A8, ANALOAF:11;
hence  u,v,u1,w are_COrte_wrt x,y by Def3; ::_thesis: verum
end;
hence  u,v,u1,w are_COrte_wrt x,y by A3; ::_thesis: verum
end;
now__::_thesis:_(_u_=_v_implies_u,v,u1,w_are_COrte_wrt_x,y_)
assume  u = v ; ::_thesis: u,v,u1,w are_COrte_wrt x,y
then  Orte (x,y,u), Orte (x,y,v) // u1,w by ANALOAF:9;
hence  u,v,u1,w are_COrte_wrt x,y by Def3; ::_thesis: verum
end;
hence  u,v,u1,w are_COrte_wrt x,y by A7; ::_thesis: verum
end;

theorem :: ANALORT:37
for V being RealLinearSpace
for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y holds
u,v,u1,w are_COrtm_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y holds
u,v,u1,w are_COrtm_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; ::_thesis: ( Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y implies u,v,u1,w are_COrtm_wrt x,y )
assume A1: Gen x,y ; ::_thesis: ( not u,v,u1,v1 are_COrtm_wrt x,y or not u,v,v1,w are_COrtm_wrt x,y or u,v,u1,w are_COrtm_wrt x,y )
assume that
A2: u,v,u1,v1 are_COrtm_wrt x,y and
A3: u,v,v1,w are_COrtm_wrt x,y ; ::_thesis: u,v,u1,w are_COrtm_wrt x,y
A4: Ortm (x,y,u), Ortm (x,y,v) // u1,v1 by A2, Def4;
A5: Ortm (x,y,u), Ortm (x,y,v) // v1,w by A3, Def4;
A6: u1,v1 // Ortm (x,y,u), Ortm (x,y,v) by A4, ANALOAF:12;
A7: now__::_thesis:_(_u_<>_v_implies_u,v,u1,w_are_COrtm_wrt_x,y_)
assume  u <> v ; ::_thesis: u,v,u1,w are_COrtm_wrt x,y
then  u1,v1 // v1,w by A1, A4, A5, Th6, ANALOAF:11;
then A8: u1,v1 // u1,w by ANALOAF:13;
now__::_thesis:_(_u1_<>_v1_implies_u,v,u1,w_are_COrtm_wrt_x,y_)
assume  u1 <> v1 ; ::_thesis: u,v,u1,w are_COrtm_wrt x,y
then  Ortm (x,y,u), Ortm (x,y,v) // u1,w by A6, A8, ANALOAF:11;
hence  u,v,u1,w are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;
hence  u,v,u1,w are_COrtm_wrt x,y by A3; ::_thesis: verum
end;
now__::_thesis:_(_u_=_v_implies_u,v,u1,w_are_COrtm_wrt_x,y_)
assume  u = v ; ::_thesis: u,v,u1,w are_COrtm_wrt x,y
then  Ortm (x,y,u), Ortm (x,y,v) // u1,w by ANALOAF:9;
hence  u,v,u1,w are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;
hence  u,v,u1,w are_COrtm_wrt x,y by A7; ::_thesis: verum
end;

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 & w,u1,u,v are_COrte_wrt x,y )
proof
let V be RealLinearSpace; ::_thesis: 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 & w,u1,u,v are_COrte_wrt x,y )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y ) )
assume A1: Gen x,y ; ::_thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
let u, v, w be VECTOR of V; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
A2: now__::_thesis:_(_u_=_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_w,u1,u,v_are_COrte_wrt_x,y_)_)
assume A3: u = v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
take u1 = w + x; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
 Orte (x,y,w), Orte (x,y,u1) // u,v by A3, ANALOAF:9;
then A4: w,u1,u,v are_COrte_wrt x,y by Def3;
now__::_thesis:_not_w_=_u1
assume  w = u1 ; ::_thesis: contradiction
then  x = 0. V by RLVECT_1:9;
hence  contradiction by A1, Lm4; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_u_<>_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_w,u1,u,v_are_COrte_wrt_x,y_)_)
assume A5: u <> v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A6: Orte (x,y,u2) = u by A1, Th15;
consider v2 being VECTOR of V such that
A7: Orte (x,y,v2) = v by A1, Th15;
take u1 = (v2 + w) - u2; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y )
 u2,v2 // w,u1 by ANALOAF:16;
then  w,u1 // u2,v2 by ANALOAF:12;
then  Orte (x,y,w), Orte (x,y,u1) // Orte (x,y,u2), Orte (x,y,v2) by A1, Th16;
then A8: w,u1,u,v are_COrte_wrt x,y by A6, A7, Def3;
now__::_thesis:_not_w_=_u1
assume  w = u1 ; ::_thesis: contradiction
then  w = w + (v2 - u2) by RLVECT_1:def_3;
then  v2 - u2 = 0. V by RLVECT_1:9;
hence  contradiction by A5, A6, A7, RLVECT_1:21; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y ) by A8; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrte_wrt x,y ) by A2; ::_thesis: verum
end;

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 & w,u1,u,v are_COrtm_wrt x,y )
proof
let V be RealLinearSpace; ::_thesis: 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 & w,u1,u,v are_COrtm_wrt x,y )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )
assume A1: Gen x,y ; ::_thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
let u, v, w be VECTOR of V; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
A2: now__::_thesis:_(_u_=_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_w,u1,u,v_are_COrtm_wrt_x,y_)_)
assume A3: u = v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
take u1 = w + x; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
 Ortm (x,y,w), Ortm (x,y,u1) // u,v by A3, ANALOAF:9;
then A4: w,u1,u,v are_COrtm_wrt x,y by Def4;
now__::_thesis:_not_w_=_u1
assume  w = u1 ; ::_thesis: contradiction
then  x = 0. V by RLVECT_1:9;
hence  contradiction by A1, Lm4; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_u_<>_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_w,u1,u,v_are_COrtm_wrt_x,y_)_)
assume A5: u <> v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A6: Ortm (x,y,u2) = u by A1, Th8;
consider v2 being VECTOR of V such that
A7: Ortm (x,y,v2) = v by A1, Th8;
take u1 = (v2 + w) - u2; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )
 u2,v2 // w,u1 by ANALOAF:16;
then  w,u1 // u2,v2 by ANALOAF:12;
then  Ortm (x,y,w), Ortm (x,y,u1) // Ortm (x,y,u2), Ortm (x,y,v2) by A1, Th17;
then A8: w,u1,u,v are_COrtm_wrt x,y by A6, A7, Def4;
now__::_thesis:_not_w_=_u1
assume  w = u1 ; ::_thesis: contradiction
then  w = w + (v2 - u2) by RLVECT_1:def_3;
then  v2 - u2 = 0. V by RLVECT_1:9;
hence  contradiction by A5, A6, A7, RLVECT_1:21; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A8; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A2; ::_thesis: verum
end;

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 & u,v,w,u1 are_COrte_wrt x,y )
proof
let V be RealLinearSpace; ::_thesis: 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 & u,v,w,u1 are_COrte_wrt x,y )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )
assume A1: Gen x,y ; ::_thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
let u, v, w be VECTOR of V; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
A2: now__::_thesis:_(_u_=_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_u,v,w,u1_are_COrte_wrt_x,y_)_)
assume A3: u = v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
take u1 = w + x; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
 Orte (x,y,u), Orte (x,y,v) // w,u1 by A3, ANALOAF:9;
then A4: u,v,w,u1 are_COrte_wrt x,y by Def3;
now__::_thesis:_not_w_=_u1
assume  w = u1 ; ::_thesis: contradiction
then  x = 0. V by RLVECT_1:9;
hence  contradiction by A1, Lm4; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_u_<>_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_u,v,w,u1_are_COrte_wrt_x,y_)_)
assume A5: u <> v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A6: Orte (x,y,u2) = u by A1, Th15;
consider v2 being VECTOR of V such that
A7: Orte (x,y,v2) = v by A1, Th15;
take u1 = (u2 + w) - v2; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
 v2,u2 // w,u1 by ANALOAF:16;
then  Orte (x,y,v2), Orte (x,y,u2) // Orte (x,y,w), Orte (x,y,u1) by A1, Th16;
then  Orte (x,y,w), Orte (x,y,u1) // v,u by A6, A7, ANALOAF:12;
then  Orte (x,y,u1), Orte (x,y,w) // u,v by ANALOAF:12;
then A8: u1,w,u,v are_COrte_wrt x,y by Def3;
now__::_thesis:_not_w_=_u1
assume  w = u1 ; ::_thesis: contradiction
then  w = w + (u2 - v2) by RLVECT_1:def_3;
then  u2 - v2 = 0. V by RLVECT_1:9;
hence  contradiction by A5, A6, A7, RLVECT_1:21; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) by A1, A8, Th18; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) by A2; ::_thesis: verum
end;

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 & u,v,w,u1 are_COrtm_wrt x,y )
proof
let V be RealLinearSpace; ::_thesis: 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 & u,v,w,u1 are_COrtm_wrt x,y )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) )
assume A1: Gen x,y ; ::_thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
let u, v, w be VECTOR of V; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
A2: now__::_thesis:_(_u_=_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_u,v,w,u1_are_COrtm_wrt_x,y_)_)
assume A3: u = v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
take u1 = w + x; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
 Ortm (x,y,w), Ortm (x,y,u1) // u,v by A3, ANALOAF:9;
then A4: w,u1,u,v are_COrtm_wrt x,y by Def4;
 w <> u1
proof
assume  w = u1 ; ::_thesis: contradiction
then  x = 0. V by RLVECT_1:9;
hence  contradiction by A1, Lm4; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) by A1, A4, Th19; ::_thesis: verum
end;
now__::_thesis:_(_u_<>_v_implies_ex_u1_being_M2(_the_carrier_of_V)_ex_u1_being_VECTOR_of_V_st_
(_w_<>_u1_&_u,v,w,u1_are_COrtm_wrt_x,y_)_)
assume A5: u <> v ; ::_thesis: ex u1 being M2( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A6: Ortm (x,y,u2) = u by A1, Th8;
consider v2 being VECTOR of V such that
A7: Ortm (x,y,v2) = v by A1, Th8;
take u1 = (v2 + w) - u2; ::_thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
 u2,v2 // w,u1 by ANALOAF:16;
then  w,u1 // u2,v2 by ANALOAF:12;
then  Ortm (x,y,w), Ortm (x,y,u1) // Ortm (x,y,u2), Ortm (x,y,v2) by A1, Th17;
then A8: w,u1,u,v are_COrtm_wrt x,y by A6, A7, Def4;
 w <> u1
proof
assume  w = u1 ; ::_thesis: contradiction
then  w = w + (v2 - u2) by RLVECT_1:def_3;
then  v2 - u2 = 0. V by RLVECT_1:9;
hence  contradiction by A5, A6, A7, RLVECT_1:21; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) by A1, A8, Th19; ::_thesis: verum
end;
hence  ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) by A2; ::_thesis: verum
end;

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 & u,u1,v,v1 are_COrte_wrt x,y & w,w1,v,v1 are_COrte_wrt x,y & w,w1,u2,v2 are_COrte_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrte_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & w,w1,v,v1 are_COrte_wrt x,y & w,w1,u2,v2 are_COrte_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrte_wrt x,y
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & w,w1,v,v1 are_COrte_wrt x,y & w,w1,u2,v2 are_COrte_wrt x,y & not w = w1 & not v = v1 implies u,u1,u2,v2 are_COrte_wrt x,y )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrte_wrt x,y or not w,w1,v,v1 are_COrte_wrt x,y or not w,w1,u2,v2 are_COrte_wrt x,y or w = w1 or v = v1 or u,u1,u2,v2 are_COrte_wrt x,y )
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: w,w1,v,v1 are_COrte_wrt x,y and
A4: w,w1,u2,v2 are_COrte_wrt x,y ; ::_thesis: ( w = w1 or v = v1 or u,u1,u2,v2 are_COrte_wrt x,y )
 Orte (x,y,u), Orte (x,y,u1) // v,v1 by A2, Def3;
then A5: v,v1 // Orte (x,y,u), Orte (x,y,u1) by ANALOAF:12;
 Orte (x,y,w), Orte (x,y,w1) // v,v1 by A3, Def3;
then A6: v,v1 // Orte (x,y,w), Orte (x,y,w1) by ANALOAF:12;
A7: Orte (x,y,w), Orte (x,y,w1) // u2,v2 by A4, Def3;
now__::_thesis:_(_w_<>_w1_&_v_<>_v1_implies_u,u1,u2,v2_are_COrte_wrt_x,y_)
assume that
A8: w <> w1 and
A9: v <> v1 ; ::_thesis: u,u1,u2,v2 are_COrte_wrt x,y
 Orte (x,y,w), Orte (x,y,w1) // Orte (x,y,u), Orte (x,y,u1) by A5, A6, A9, ANALOAF:11;
then  Orte (x,y,u), Orte (x,y,u1) // u2,v2 by A1, A7, A8, Th13, ANALOAF:11;
hence  u,u1,u2,v2 are_COrte_wrt x,y by Def3; ::_thesis: verum
end;
hence  ( w = w1 or v = v1 or u,u1,u2,v2 are_COrte_wrt x,y ) ; ::_thesis: verum
end;

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 & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrtm_wrt x,y
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrtm_wrt x,y
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 implies u,u1,u2,v2 are_COrtm_wrt x,y )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or not w,w1,v,v1 are_COrtm_wrt x,y or not w,w1,u2,v2 are_COrtm_wrt x,y or w = w1 or v = v1 or u,u1,u2,v2 are_COrtm_wrt x,y )
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: w,w1,v,v1 are_COrtm_wrt x,y and
A4: w,w1,u2,v2 are_COrtm_wrt x,y ; ::_thesis: ( w = w1 or v = v1 or u,u1,u2,v2 are_COrtm_wrt x,y )
 Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by A2, Def4;
then A5: v,v1 // Ortm (x,y,u), Ortm (x,y,u1) by ANALOAF:12;
 Ortm (x,y,w), Ortm (x,y,w1) // v,v1 by A3, Def4;
then A6: v,v1 // Ortm (x,y,w), Ortm (x,y,w1) by ANALOAF:12;
A7: Ortm (x,y,w), Ortm (x,y,w1) // u2,v2 by A4, Def4;
now__::_thesis:_(_w_<>_w1_&_v_<>_v1_implies_u,u1,u2,v2_are_COrtm_wrt_x,y_)
assume that
A8: w <> w1 and
A9: v <> v1 ; ::_thesis: u,u1,u2,v2 are_COrtm_wrt x,y
 Ortm (x,y,w), Ortm (x,y,w1) // Ortm (x,y,u), Ortm (x,y,u1) by A5, A6, A9, ANALOAF:11;
then  Ortm (x,y,u), Ortm (x,y,u1) // u2,v2 by A1, A7, A8, Th6, ANALOAF:11;
hence  u,u1,u2,v2 are_COrtm_wrt x,y by Def4; ::_thesis: verum
end;
hence  ( w = w1 or v = v1 or u,u1,u2,v2 are_COrtm_wrt x,y ) ; ::_thesis: verum
end;

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 & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 holds
w = w1
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 holds
w = w1
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 implies w = w1 )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrte_wrt x,y or not v,v1,w,w1 are_COrte_wrt x,y or not u2,v2,w,w1 are_COrte_wrt x,y or u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: v,v1,w,w1 are_COrte_wrt x,y and
A4: u2,v2,w,w1 are_COrte_wrt x,y ; ::_thesis: ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
 v,v1,u1,u are_COrte_wrt x,y by A1, A2, Th18;
then A5: Orte (x,y,v), Orte (x,y,v1) // u1,u by Def3;
 Orte (x,y,v), Orte (x,y,v1) // w,w1 by A3, Def3;
then A6: w,w1 // Orte (x,y,v), Orte (x,y,v1) by ANALOAF:12;
 Orte (x,y,u2), Orte (x,y,v2) // w,w1 by A4, Def3;
then A7: w,w1 // Orte (x,y,u2), Orte (x,y,v2) by ANALOAF:12;
now__::_thesis:_(_w_<>_w1_&_v_<>_v1_&_not_u,u1,u2,v2_are_COrte_wrt_x,y_&_not_v_=_v1_implies_w_=_w1_)
assume that
A8: w <> w1 and
A9: v <> v1 ; ::_thesis: ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
 Orte (x,y,v), Orte (x,y,v1) // Orte (x,y,u2), Orte (x,y,v2) by A6, A7, A8, ANALOAF:11;
then  Orte (x,y,u2), Orte (x,y,v2) // u1,u by A1, A5, A9, Th13, ANALOAF:11;
then  Orte (x,y,v2), Orte (x,y,u2) // u,u1 by ANALOAF:12;
then  v2,u2,u,u1 are_COrte_wrt x,y by Def3;
hence  ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 ) by A1, Th18; ::_thesis: verum
end;
hence  ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 ) ; ::_thesis: verum
end;

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 & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 holds
w = w1
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 holds
w = w1
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 implies w = w1 )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or not v,v1,w,w1 are_COrtm_wrt x,y or not u2,v2,w,w1 are_COrtm_wrt x,y or u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: v,v1,w,w1 are_COrtm_wrt x,y and
A4: u2,v2,w,w1 are_COrtm_wrt x,y ; ::_thesis: ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
 Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by A2, Def4;
then A5: v,v1 // Ortm (x,y,u), Ortm (x,y,u1) by ANALOAF:12;
 w,w1,v,v1 are_COrtm_wrt x,y by A1, A3, Th19;
then  Ortm (x,y,w), Ortm (x,y,w1) // v,v1 by Def4;
then A6: v,v1 // Ortm (x,y,w), Ortm (x,y,w1) by ANALOAF:12;
 w,w1,u2,v2 are_COrtm_wrt x,y by A1, A4, Th19;
then A7: Ortm (x,y,w), Ortm (x,y,w1) // u2,v2 by Def4;
now__::_thesis:_(_w_<>_w1_&_v_<>_v1_&_not_u,u1,u2,v2_are_COrtm_wrt_x,y_&_not_v_=_v1_implies_w_=_w1_)
assume that
A8: w <> w1 and
A9: v <> v1 ; ::_thesis: ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
 Ortm (x,y,w), Ortm (x,y,w1) // Ortm (x,y,u), Ortm (x,y,u1) by A5, A6, A9, ANALOAF:11;
then  Ortm (x,y,u), Ortm (x,y,u1) // u2,v2 by A1, A7, A8, Th6, ANALOAF:11;
hence  ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 ) by Def4; ::_thesis: verum
end;
hence  ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 ) ; ::_thesis: verum
end;

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 & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u,u1,u2,v2 are_COrte_wrt x,y & not u2,v2,w,w1 are_COrte_wrt x,y & not v = v1 holds
u = u1
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u,u1,u2,v2 are_COrte_wrt x,y & not u2,v2,w,w1 are_COrte_wrt x,y & not v = v1 holds
u = u1
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u,u1,u2,v2 are_COrte_wrt x,y & not u2,v2,w,w1 are_COrte_wrt x,y & not v = v1 implies u = u1 )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrte_wrt x,y or not v,v1,w,w1 are_COrte_wrt x,y or not u,u1,u2,v2 are_COrte_wrt x,y or u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: v,v1,w,w1 are_COrte_wrt x,y and
A4: u,u1,u2,v2 are_COrte_wrt x,y ; ::_thesis: ( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )
A5: Orte (x,y,u), Orte (x,y,u1) // v,v1 by A2, Def3;
A6: Orte (x,y,v), Orte (x,y,v1) // w,w1 by A3, Def3;
A7: Orte (x,y,u), Orte (x,y,u1) // u2,v2 by A4, Def3;
now__::_thesis:_(_u_<>_u1_&_v_<>_v1_&_not_u2,v2,w,w1_are_COrte_wrt_x,y_&_not_v_=_v1_implies_u_=_u1_)
assume that
A8: u <> u1 and
A9: v <> v1 ; ::_thesis: ( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )
 v,v1 // u2,v2 by A1, A5, A7, A8, Th13, ANALOAF:11;
then  Orte (x,y,v), Orte (x,y,v1) // Orte (x,y,u2), Orte (x,y,v2) by A1, Th16;
then  Orte (x,y,u2), Orte (x,y,v2) // w,w1 by A1, A6, A9, Th13, ANALOAF:11;
hence  ( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 ) by Def3; ::_thesis: verum
end;
hence  ( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 ) ; ::_thesis: verum
end;

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 & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 holds
u = u1
proof
let V be RealLinearSpace; ::_thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 holds
u = u1
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; ::_thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y & not u2,v2,w,w1 are_COrtm_wrt x,y & not v = v1 implies u = u1 )
assume A1: Gen x,y ; ::_thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or not v,v1,w,w1 are_COrtm_wrt x,y or not u,u1,u2,v2 are_COrtm_wrt x,y or u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 )
assume that
A2: u,u1,v,v1 are_COrtm_wrt x,y and
A3: v,v1,w,w1 are_COrtm_wrt x,y and
A4: u,u1,u2,v2 are_COrtm_wrt x,y ; ::_thesis: ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 )
A5: Ortm (x,y,u), Ortm (x,y,u1) // v,v1 by A2, Def4;
A6: Ortm (x,y,v), Ortm (x,y,v1) // w,w1 by A3, Def4;
A7: Ortm (x,y,u), Ortm (x,y,u1) // u2,v2 by A4, Def4;
now__::_thesis:_(_u_<>_u1_&_v_<>_v1_&_not_u2,v2,w,w1_are_COrtm_wrt_x,y_&_not_v_=_v1_implies_u_=_u1_)
assume that
A8: u <> u1 and
A9: v <> v1 ; ::_thesis: ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 )
 v,v1 // u2,v2 by A1, A5, A7, A8, Th6, ANALOAF:11;
then  Ortm (x,y,v), Ortm (x,y,v1) // Ortm (x,y,u2), Ortm (x,y,v2) by A1, Th17;
then  Ortm (x,y,u2), Ortm (x,y,v2) // w,w1 by A1, A6, A9, Th6, ANALOAF:11;
hence  ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 ) by Def4; ::_thesis: verum
end;
hence  ( u2,v2,w,w1 are_COrtm_wrt x,y or v = v1 or u = u1 ) ; ::_thesis: verum
end;

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 & not v,v1,u1,w are_COrte_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
proof
let V be RealLinearSpace; ::_thesis: 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 & not v,v1,u1,w are_COrte_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) ) )
assume A1: Gen x,y ; ::_thesis: for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
let v, w, u1, v1, w1 be VECTOR of V; ::_thesis: ( not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y implies 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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) ) )
consider u being VECTOR of V such that
A2: v <> u and
A3: v,v1,v,u are_COrte_wrt x,y by A1, Th40;
assume that
A4: not v,v1,w,u1 are_COrte_wrt x,y and
A5: not v,v1,u1,w are_COrte_wrt x,y and
A6: u1,w1,u1,w are_COrte_wrt x,y ; ::_thesis: 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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
A7: not Orte (x,y,v), Orte (x,y,v1) // w,u1 by A4, Def3;
A8: Orte (x,y,v), Orte (x,y,v1) // v,u by A3, Def3;
A9: Orte (x,y,u1), Orte (x,y,w1) // u1,w by A6, Def3;
A10: not Orte (x,y,v), Orte (x,y,v1) // u1,w by A5, Def3;
A11: v,u // Orte (x,y,v), Orte (x,y,v1) by A8, ANALOAF:12;
A12: u1,w // Orte (x,y,u1), Orte (x,y,w1) by A9, ANALOAF:12;
A13: u1 <> w by A7, ANALOAF:9;
A14: not v,u // u1,w by A2, A10, A11, ANALOAF:11;
A15: not v,u // w,u1 by A2, A7, A11, ANALOAF:11;
 ( Gen x,y implies ex u, v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * u) + (b * v) = w )
proof
assume A16: Gen x,y ; ::_thesis: ex u, v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * u) + (b * v) = w
take  x ; ::_thesis: ex v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * x) + (b * v) = w
take  y ; ::_thesis: for w being VECTOR of V ex a, b being Real st (a * x) + (b * y) = w
thus  for w being VECTOR of V ex a, b being Real st (a * x) + (b * y) = w by A16, ANALMETR:def_1; ::_thesis: verum
end;
then consider u2 being VECTOR of V such that
A17: ( v,u // v,u2 or v,u // u2,v ) and
A18: ( u1,w // u1,u2 or u1,w // u2,u1 ) by A1, A14, A15, ANALOAF:21;
 ( Orte (x,y,v), Orte (x,y,v1) // v,u2 or Orte (x,y,v), Orte (x,y,v1) // u2,v ) by A2, A11, A17, ANALOAF:11;
then A19: ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) by Def3;
 ( Orte (x,y,u1), Orte (x,y,w1) // u1,u2 or Orte (x,y,u1), Orte (x,y,w1) // u2,u1 ) by A12, A13, A18, ANALOAF:11;
then  ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) by Def3;
hence  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 ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) ) by A19; ::_thesis: verum
end;

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 & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
proof
let V be RealLinearSpace; ::_thesis: 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 & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) ) )
assume A1: Gen x,y ; ::_thesis: ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
 ( Gen x,y implies ex u, v being VECTOR of V st u <> v )
proof
assume A2: Gen x,y ; ::_thesis: ex u, v being VECTOR of V st u <> v
take  x ; ::_thesis: ex v being VECTOR of V st x <> v
take  0. V ; ::_thesis: x <> 0. V
thus  x <> 0. V by A2, Lm4; ::_thesis: verum
end;
then consider u, v being VECTOR of V such that
A3: u <> v by A1;
take  u ; ::_thesis: ex v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
take  v ; ::_thesis: ex w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
consider w being VECTOR of V such that
A4: w <> u and
A5: u,v,u,w are_COrte_wrt x,y by A1, Th40;
take  w ; ::_thesis: ( u,v,u,w are_COrte_wrt x,y & ( 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
thus  u,v,u,w are_COrte_wrt x,y by A5; ::_thesis: 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 & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A6: Orte (x,y,u), Orte (x,y,v) // u,w by A5, Def3;
let v1, w1 be VECTOR of V; ::_thesis: ( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
assume  v1,w1,u,v are_COrte_wrt x,y ; ::_thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
then A7: Orte (x,y,v1), Orte (x,y,w1) // u,v by Def3;
now__::_thesis:_(_v1_<>_w1_&_(_v1,w1,u,w_are_COrte_wrt_x,y_or_v1,w1,w,u_are_COrte_wrt_x,y_)_implies_ex_a,_b_being_Real_st_
(_(_not_v1,w1,u,w_are_COrte_wrt_x,y_&_not_v1,w1,w,u_are_COrte_wrt_x,y_)_or_v1_=_w1_)_)
assume A8: v1 <> w1 ; ::_thesis: ( ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) )
assume  ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) ; ::_thesis: ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
then  ( Orte (x,y,v1), Orte (x,y,w1) // u,w or Orte (x,y,v1), Orte (x,y,w1) // w,u ) by Def3;
then  ( u,v // u,w or u,v // w,u ) by A1, A7, A8, Th13, ANALOAF:11;
then  ( Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u), Orte (x,y,w) or Orte (x,y,u), Orte (x,y,v) // Orte (x,y,w), Orte (x,y,u) ) by A1, Th16;
then  ( u,w // Orte (x,y,u), Orte (x,y,w) or u,w // Orte (x,y,w), Orte (x,y,u) ) by A1, A3, A6, Th13, ANALOAF:11;
then consider a, b being Real such that
A9: a * (w - u) = b * ((Orte (x,y,w)) - (Orte (x,y,u))) and
A10: ( a <> 0 or b <> 0 ) by ANALMETR:14;
take a = a; ::_thesis: ex b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
take b = b; ::_thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
 a * (w - u) = b * (Orte (x,y,(w - u))) by A1, A9, Th11;
then A11: a * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = b * (Orte (x,y,(w - u))) by A1, Lm5;
A12: now__::_thesis:_(_not_a_<>_0_or_(_not_v1,w1,u,w_are_COrte_wrt_x,y_&_not_v1,w1,w,u_are_COrte_wrt_x,y_)_or_v1_=_w1_)
assume A13: a <> 0 ; ::_thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A14: pr2 (x,y,(w - u)) <> 0
proof
assume A15: not pr2 (x,y,(w - u)) <> 0 ; ::_thesis: contradiction
then  a * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by A11, Lm2;
then  ((a * (pr1 (x,y,(w - u)))) * x) + ((a * (pr2 (x,y,(w - u)))) * y) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by Lm2;
then  a * (pr1 (x,y,(w - u))) = 0 by A1, Lm3;
then  pr1 (x,y,(w - u)) = 0 by A13, XCMPLX_1:6;
then w - u = (0 * x) + (0 * y) by A1, A15, Lm5
.= (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A4, RLVECT_1:21; ::_thesis: verum
end;
 ((a ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = (a ") * (b * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y))) by A11, RLVECT_1:def_7;
then  ((a ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((a ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def_7;
then  1 * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((a ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by A13, XCMPLX_0:def_7;
then  ((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y) = ((a ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def_8;
then A16: ((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y) = ((((a ") * b) * (pr2 (x,y,(w - u)))) * x) + ((((a ") * b) * (- (pr1 (x,y,(w - u))))) * y) by Lm2;
then  pr1 (x,y,(w - u)) = ((a ") * b) * (pr2 (x,y,(w - u))) by A1, Lm3;
then A17: pr2 (x,y,(w - u)) = - (((a ") * b) * (((a ") * b) * (pr2 (x,y,(w - u))))) by A1, A16, Lm3;
- (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) = ((pr2 (x,y,(w - u))) ") * (- (pr2 (x,y,(w - u))))
.= ((pr2 (x,y,(w - u))) ") * (((a ") * b) * (((a ") * b) * (pr2 (x,y,(w - u))))) by A17 ;
then  - 1 = (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) * (((a ") * b) * ((a ") * b)) by A14, XCMPLX_0:def_7;
then  - 1 = 1 * (((a ") * b) * ((a ") * b)) by A14, XCMPLX_0:def_7;
hence  ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by XREAL_1:63; ::_thesis: verum
end;
now__::_thesis:_(_not_b_<>_0_or_(_not_v1,w1,u,w_are_COrte_wrt_x,y_&_not_v1,w1,w,u_are_COrte_wrt_x,y_)_or_v1_=_w1_)
assume A18: b <> 0 ; ::_thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A19: pr2 (x,y,(w - u)) <> 0
proof
assume A20: not pr2 (x,y,(w - u)) <> 0 ; ::_thesis: contradiction
then  a * (((pr1 (x,y,(w - u))) * x) + (0 * y)) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by A11, Lm2;
then  ((a * (pr1 (x,y,(w - u)))) * x) + ((a * 0) * y) = ((b * 0) * x) + ((b * (- (pr1 (x,y,(w - u))))) * y) by Lm2;
then  b * (- (pr1 (x,y,(w - u)))) = 0 by A1, Lm3;
then  - (pr1 (x,y,(w - u))) = 0 by A18, XCMPLX_1:6;
then w - u = (0 * x) + ((- 0) * y) by A1, A20, Lm5
.= (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A4, RLVECT_1:21; ::_thesis: verum
end;
 (b ") * (a * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y))) = ((b ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by A11, RLVECT_1:def_7;
then  ((b ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((b ") * b) * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def_7;
then  ((b ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = 1 * (((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y)) by A18, XCMPLX_0:def_7;
then  ((b ") * a) * (((pr1 (x,y,(w - u))) * x) + ((pr2 (x,y,(w - u))) * y)) = ((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y) by RLVECT_1:def_8;
then A21: ((((b ") * a) * (pr1 (x,y,(w - u)))) * x) + ((((b ") * a) * (pr2 (x,y,(w - u)))) * y) = ((pr2 (x,y,(w - u))) * x) + ((- (pr1 (x,y,(w - u)))) * y) by Lm2;
then  ((b ") * a) * (pr2 (x,y,(w - u))) = - (pr1 (x,y,(w - u))) by A1, Lm3;
then A22: pr2 (x,y,(w - u)) = ((b ") * a) * (- (((b ") * a) * (pr2 (x,y,(w - u))))) by A1, A21, Lm3;
- (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) = ((pr2 (x,y,(w - u))) ") * (- (pr2 (x,y,(w - u))))
.= ((pr2 (x,y,(w - u))) ") * (((b ") * a) * (((b ") * a) * (pr2 (x,y,(w - u))))) by A22 ;
then  - 1 = (((pr2 (x,y,(w - u))) ") * (pr2 (x,y,(w - u)))) * (((b ") * a) * ((b ") * a)) by A19, XCMPLX_0:def_7;
then  - 1 = 1 * (((b ") * a) * ((b ") * a)) by A19, XCMPLX_0:def_7;
hence  ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by XREAL_1:63; ::_thesis: verum
end;
hence  ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by A10, A12; ::_thesis: verum
end;
hence  ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ; ::_thesis: verum
end;

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 & not v,v1,u1,w are_COrtm_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
proof
let V be RealLinearSpace; ::_thesis: 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 & not v,v1,u1,w are_COrtm_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) ) )
assume A1: Gen x,y ; ::_thesis: for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & 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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
let v, w, u1, v1, w1 be VECTOR of V; ::_thesis: ( not v,v1,w,u1 are_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y implies 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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) ) )
consider u being VECTOR of V such that
A2: v <> u and
A3: v,v1,v,u are_COrtm_wrt x,y by A1, Th41;
assume that
A4: not v,v1,w,u1 are_COrtm_wrt x,y and
A5: not v,v1,u1,w are_COrtm_wrt x,y and
A6: u1,w1,u1,w are_COrtm_wrt x,y ; ::_thesis: 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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
A7: not Ortm (x,y,v), Ortm (x,y,v1) // w,u1 by A4, Def4;
A8: Ortm (x,y,v), Ortm (x,y,v1) // v,u by A3, Def4;
A9: Ortm (x,y,u1), Ortm (x,y,w1) // u1,w by A6, Def4;
A10: not Ortm (x,y,v), Ortm (x,y,v1) // u1,w by A5, Def4;
A11: v,u // Ortm (x,y,v), Ortm (x,y,v1) by A8, ANALOAF:12;
A12: u1,w // Ortm (x,y,u1), Ortm (x,y,w1) by A9, ANALOAF:12;
A13: u1 <> w by A7, ANALOAF:9;
A14: not v,u // u1,w by A2, A10, A11, ANALOAF:11;
A15: not v,u // w,u1 by A2, A7, A11, ANALOAF:11;
 ( Gen x,y implies ex u, v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * u) + (b * v) = w )
proof
assume A16: Gen x,y ; ::_thesis: ex u, v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * u) + (b * v) = w
take  x ; ::_thesis: ex v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * x) + (b * v) = w
take  y ; ::_thesis: for w being VECTOR of V ex a, b being Real st (a * x) + (b * y) = w
thus  for w being VECTOR of V ex a, b being Real st (a * x) + (b * y) = w by A16, ANALMETR:def_1; ::_thesis: verum
end;
then consider u2 being VECTOR of V such that
A17: ( v,u // v,u2 or v,u // u2,v ) and
A18: ( u1,w // u1,u2 or u1,w // u2,u1 ) by A1, A14, A15, ANALOAF:21;
 ( Ortm (x,y,v), Ortm (x,y,v1) // v,u2 or Ortm (x,y,v), Ortm (x,y,v1) // u2,v ) by A2, A11, A17, ANALOAF:11;
then A19: ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) by Def4;
 ( Ortm (x,y,u1), Ortm (x,y,w1) // u1,u2 or Ortm (x,y,u1), Ortm (x,y,w1) // u2,u1 ) by A12, A13, A18, ANALOAF:11;
then  ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) by Def4;
hence  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 ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) ) by A19; ::_thesis: verum
end;

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 & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
proof
let V be RealLinearSpace; ::_thesis: 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 & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) ) )
assume A1: Gen x,y ; ::_thesis: ex u, v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take u = (0 * x) + (0 * y); ::_thesis: ex v, w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take v = (1 * x) + (1 * y); ::_thesis: ex w being VECTOR of V st
( u,v,u,w are_COrtm_wrt x,y & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
take w = (1 * x) + ((- 1) * y); ::_thesis: ( u,v,u,w are_COrtm_wrt x,y & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) )
A2: pr1 (x,y,u) = 0 by A1, Lm6;
A3: pr2 (x,y,u) = 0 by A1, Lm6;
A4: pr1 (x,y,v) = 1 by A1, Lm6;
 pr2 (x,y,v) = 1 by A1, Lm6;
then A5: Ortm (x,y,u), Ortm (x,y,v) // u,w by A2, A3, A4, ANALOAF:8;
 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
proof
let v1, w1 be VECTOR of V; ::_thesis: ( not v1,w1,u,v are_COrtm_wrt x,y or ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
assume  v1,w1,u,v are_COrtm_wrt x,y ; ::_thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
then A6: Ortm (x,y,v1), Ortm (x,y,w1) // u,v by Def4;
now__::_thesis:_(_v1_<>_w1_&_(_v1,w1,u,w_are_COrtm_wrt_x,y_or_v1,w1,w,u_are_COrtm_wrt_x,y_)_implies_ex_a,_b_being_Real_st_
(_(_not_v1,w1,u,w_are_COrtm_wrt_x,y_&_not_v1,w1,w,u_are_COrtm_wrt_x,y_)_or_v1_=_w1_)_)
assume A7: v1 <> w1 ; ::_thesis: ( ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) )
assume  ( v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y ) ; ::_thesis: ex a, b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
then  ( Ortm (x,y,v1), Ortm (x,y,w1) // u,w or Ortm (x,y,v1), Ortm (x,y,w1) // w,u ) by Def4;
then  ( u,v // u,w or u,v // w,u ) by A1, A6, A7, Th6, ANALOAF:11;
then consider a, b being Real such that
A8: a * (v - u) = b * (w - u) and
A9: ( a <> 0 or b <> 0 ) by ANALMETR:14;
take a = a; ::_thesis: ex b being Real st
( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
take b = b; ::_thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
u = (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then  a * v = b * (w - (0. V)) by A8, RLVECT_1:13;
then A10: a * v = b * w by RLVECT_1:13;
A11: now__::_thesis:_(_not_a_<>_0_or_(_not_v1,w1,u,w_are_COrtm_wrt_x,y_&_not_v1,w1,w,u_are_COrtm_wrt_x,y_)_or_v1_=_w1_)
assume A12: a <> 0 ; ::_thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
 ((a ") * a) * v = (a ") * (b * w) by A10, RLVECT_1:def_7;
then  ((a ") * a) * v = ((a ") * b) * w by RLVECT_1:def_7;
then  1 * v = ((a ") * b) * w by A12, XCMPLX_0:def_7;
then  1 * v = ((((a ") * b) * 1) * x) + ((((a ") * b) * (- 1)) * y) by Lm2;
then A13: ((1 * 1) * x) + ((1 * 1) * y) = ((((a ") * b) * 1) * x) + ((((a ") * b) * (- 1)) * y) by Lm2;
then  a * 1 = a * ((a ") * (b * 1)) by A1, Lm3;
then A14: a * 1 = (a * (a ")) * (b * 1) ;
 1 = ((a ") * b) * (- 1) by A1, A13, Lm3;
then  1 = ((a ") * a) * (- 1) by A12, A14, XCMPLX_0:def_7;
hence  ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) by A12, XCMPLX_0:def_7; ::_thesis: verum
end;
now__::_thesis:_(_not_b_<>_0_or_(_not_v1,w1,u,w_are_COrtm_wrt_x,y_&_not_v1,w1,w,u_are_COrtm_wrt_x,y_)_or_v1_=_w1_)
assume A15: b <> 0 ; ::_thesis: ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 )
 ((b ") * a) * v = (b ") * (b * w) by A10, RLVECT_1:def_7;
then  ((b ") * a) * v = ((b ") * b) * w by RLVECT_1:def_7;
then  ((b ") * a) * v = 1 * w by A15, XCMPLX_0:def_7;
then  ((((b ") * a) * 1) * x) + ((((b ") * a) * 1) * y) = 1 * w by Lm2;
then A16: ((((b ") * a) * 1) * x) + ((((b ") * a) * 1) * y) = ((1 * 1) * x) + ((1 * (- 1)) * y) by Lm2;
then  b * 1 = b * ((b ") * (a * 1)) by A1, Lm3;
then A17: b * 1 = (b * (b ")) * (a * 1) ;
 - 1 = ((b ") * a) * 1 by A1, A16, Lm3;
then  - 1 = ((b ") * b) * 1 by A15, A17, XCMPLX_0:def_7;
hence  ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) by A15, XCMPLX_0:def_7; ::_thesis: verum
end;
hence  ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) by A9, A11; ::_thesis: verum
end;
hence  ( ( not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ; ::_thesis: verum
end;
hence  ( u,v,u,w are_COrtm_wrt x,y & ( 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 & not v1,w1,w,u are_COrtm_wrt x,y ) or v1 = w1 ) ) ) by A5, Def4; ::_thesis: verum
end;


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] & vv = [v1,v2] & 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] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )
proof
set VV = [: the carrier of V, the carrier of V:];
defpred S1[ set , set ] means  ex u1, u2, v1, v2 being VECTOR of V st
( $1 = [u1,u2] & $2 = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y );
consider P being Relation of [: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:] such that
A1: for uu, vv being set holds
( [uu,vv] in P iff ( uu in [: the carrier of V, the carrier of V:] & vv in [: the carrier of V, the carrier of V:] & S1[uu,vv] ) ) from RELSET_1:sch_1();
take  P ; ::_thesis: for uu, vv being set holds
( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )
let uu, vv be set ; ::_thesis: ( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )
thus  ( [uu,vv] in P implies ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) by A1; ::_thesis: ( ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) implies [uu,vv] in P )
assume A2: ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ; ::_thesis: [uu,vv] in P
then A3: uu in [: the carrier of V, the carrier of V:] by ZFMISC_1:def_2;
 vv in [: the carrier of V, the carrier of V:] by A2, ZFMISC_1:def_2;
hence  [uu,vv] in P by A1, A2, A3; ::_thesis: verum
end;
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] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) & ( for uu, vv being set holds
( [uu,vv] in b2 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) holds
b1 = b2
proof
let P, Q be Relation of [: the carrier of V, the carrier of V:]; ::_thesis: ( ( for uu, vv being set holds
( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) & ( for uu, vv being set holds
( [uu,vv] in Q iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ) implies P = Q )
assume that
A4: for uu, vv being set holds
( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) and
A5: for uu, vv being set holds
( [uu,vv] in Q iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) ; ::_thesis: P = Q
 for uu, vv being set holds
( [uu,vv] in P iff [uu,vv] in Q )
proof
let uu, vv be set ; ::_thesis: ( [uu,vv] in P iff [uu,vv] in Q )
 ( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) by A4;
hence  ( [uu,vv] in P iff [uu,vv] in Q ) by A5; ::_thesis: verum
end;
hence  P = Q by RELAT_1:def_2; ::_thesis: verum
end;
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] & vv = [v1,v2] & 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] & vv = [v1,v2] & 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] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) )
proof
set VV = [: the carrier of V, the carrier of V:];
defpred S1[ set , set ] means  ex u1, u2, v1, v2 being VECTOR of V st
( $1 = [u1,u2] & $2 = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y );
consider P being Relation of [: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:] such that
A1: for uu, vv being set holds
( [uu,vv] in P iff ( uu in [: the carrier of V, the carrier of V:] & vv in [: the carrier of V, the carrier of V:] & S1[uu,vv] ) ) from RELSET_1:sch_1();
take  P ; ::_thesis: for uu, vv being set holds
( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) )
let uu, vv be set ; ::_thesis: ( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) )
thus  ( [uu,vv] in P implies ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) by A1; ::_thesis: ( ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) implies [uu,vv] in P )
assume A2: ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ; ::_thesis: [uu,vv] in P
then A3: uu in [: the carrier of V, the carrier of V:] by ZFMISC_1:def_2;
 vv in [: the carrier of V, the carrier of V:] by A2, ZFMISC_1:def_2;
hence  [uu,vv] in P by A1, A2, A3; ::_thesis: verum
end;
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] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) & ( for uu, vv being set holds
( [uu,vv] in b2 iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) holds
b1 = b2
proof
let P, Q be Relation of [: the carrier of V, the carrier of V:]; ::_thesis: ( ( for uu, vv being set holds
( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) & ( for uu, vv being set holds
( [uu,vv] in Q iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ) implies P = Q )
assume that
A4: for uu, vv being set holds
( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) and
A5: for uu, vv being set holds
( [uu,vv] in Q iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) ; ::_thesis: P = Q
 for uu, vv being set holds
( [uu,vv] in P iff [uu,vv] in Q )
proof
let uu, vv be set ; ::_thesis: ( [uu,vv] in P iff [uu,vv] in Q )
 ( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st
( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y ) ) by A4;
hence  ( [uu,vv] in P iff [uu,vv] in Q ) by A5; ::_thesis: verum
end;
hence  P = Q by RELAT_1:def_2; ::_thesis: verum
end;
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] & vv = [v1,v2] & 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 & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
proof
let V be RealLinearSpace; ::_thesis: 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 & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
let u, v, u1, v1, x, y be VECTOR of V; ::_thesis: for p, q, r, s being Element of (CESpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
let p, q, r, s be Element of (CESpace (V,x,y)); ::_thesis: ( u = p & v = q & u1 = r & v1 = s implies ( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y ) )
assume that
A1: u = p and
A2: v = q and
A3: u1 = r and
A4: v1 = s ; ::_thesis: ( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y )
A5: ( p,q // r,s implies u,v,u1,v1 are_COrte_wrt x,y )
proof
assume  p,q // r,s ; ::_thesis: u,v,u1,v1 are_COrte_wrt x,y
then  [[p,q],[r,s]] in the CONGR of (CESpace (V,x,y)) by ANALOAF:def_2;
then consider u19, u29, v19, v29 being VECTOR of V such that
A6: [u,v] = [u19,u29] and
A7: [u1,v1] = [v19,v29] and
A8: u19,u29,v19,v29 are_COrte_wrt x,y by A1, A2, A3, A4, Def5;
A9: u = u19 by A6, XTUPLE_0:1;
A10: v = u29 by A6, XTUPLE_0:1;
 u1 = v19 by A7, XTUPLE_0:1;
hence  u,v,u1,v1 are_COrte_wrt x,y by A7, A8, A9, A10, XTUPLE_0:1; ::_thesis: verum
end;
 ( u,v,u1,v1 are_COrte_wrt x,y implies p,q // r,s )
proof
assume  u,v,u1,v1 are_COrte_wrt x,y ; ::_thesis: p,q // r,s
then  [[u,v],[u1,v1]] in the CONGR of AffinStruct(# the carrier of V,(CORTE (V,x,y)) #) by Def5;
hence  p,q // r,s by A1, A2, A3, A4, ANALOAF:def_2; ::_thesis: verum
end;
hence  ( p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y ) by A5; ::_thesis: verum
end;


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 & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
proof
let V be RealLinearSpace; ::_thesis: 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 & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
let u, v, u1, v1, x, y be VECTOR of V; ::_thesis: for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
let p, q, r, s be Element of (CMSpace (V,x,y)); ::_thesis: ( u = p & v = q & u1 = r & v1 = s implies ( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) )
assume that
A1: u = p and
A2: v = q and
A3: u1 = r and
A4: v1 = s ; ::_thesis: ( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
A5: ( p,q // r,s implies u,v,u1,v1 are_COrtm_wrt x,y )
proof
assume  p,q // r,s ; ::_thesis: u,v,u1,v1 are_COrtm_wrt x,y
then  [[p,q],[r,s]] in the CONGR of (CMSpace (V,x,y)) by ANALOAF:def_2;
then consider u19, u29, v19, v29 being VECTOR of V such that
A6: [u,v] = [u19,u29] and
A7: [u1,v1] = [v19,v29] and
A8: u19,u29,v19,v29 are_COrtm_wrt x,y by A1, A2, A3, A4, Def6;
A9: u = u19 by A6, XTUPLE_0:1;
A10: v = u29 by A6, XTUPLE_0:1;
 u1 = v19 by A7, XTUPLE_0:1;
hence  u,v,u1,v1 are_COrtm_wrt x,y by A7, A8, A9, A10, XTUPLE_0:1; ::_thesis: verum
end;
 ( u,v,u1,v1 are_COrtm_wrt x,y implies p,q // r,s )
proof
assume  u,v,u1,v1 are_COrtm_wrt x,y ; ::_thesis: p,q // r,s
then  [[u,v],[u1,v1]] in the CONGR of AffinStruct(# the carrier of V,(CORTM (V,x,y)) #) by Def6;
hence  p,q // r,s by A1, A2, A3, A4, ANALOAF:def_2; ::_thesis: verum
end;
hence  ( p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) by A5; ::_thesis: verum
end;