:: ANALOAF semantic presentation

begin


definition
let V be RealLinearSpace;
let u, v, w, y be VECTOR of V;
predu,v // w,y means :Def1: :: ANALOAF:def 1
( u = v or w = y or ex a, b being Real st
( 0 < a & 0 < b & a * (v - u) = b * (y - w) ) );
end;

:: deftheorem Def1 defines // ANALOAF:def_1_:_
 for V being RealLinearSpace
for u, v, w, y being VECTOR of V holds
( u,v // w,y iff ( u = v or w = y or ex a, b being Real st
( 0 < a & 0 < b & a * (v - u) = b * (y - w) ) ) );

theorem Th1: :: ANALOAF:1
for V being RealLinearSpace
for w, v, u being VECTOR of V holds (w - v) + (v - u) = w - u
proof
let V be RealLinearSpace; ::_thesis: for w, v, u being VECTOR of V holds (w - v) + (v - u) = w - u
let w, v, u be VECTOR of V; ::_thesis: (w - v) + (v - u) = w - u
thus (w - v) + (v - u) = w - (v - (v - u)) by RLVECT_1:29
.= w - ((v - v) + u) by RLVECT_1:29
.= w - ((0. V) + u) by RLVECT_1:15
.= w - u by RLVECT_1:4 ; ::_thesis: verum
end;

theorem Th2: :: ANALOAF:2
for V being RealLinearSpace
for y, u, v, w being VECTOR of V st y + u = v + w holds
y - w = v - u
proof
let V be RealLinearSpace; ::_thesis: for y, u, v, w being VECTOR of V st y + u = v + w holds
y - w = v - u
let y, u, v, w be VECTOR of V; ::_thesis: ( y + u = v + w implies y - w = v - u )
assume A1: y + u = v + w ; ::_thesis: y - w = v - u
thus y - w = (y + (0. V)) - w by RLVECT_1:4
.= (y + (u - u)) - w by RLVECT_1:15
.= ((v + w) + (- u)) - w by A1, RLVECT_1:def_3
.= (- u) + ((v + w) - w) by RLVECT_1:def_3
.= v - u by RLSUB_2:61 ; ::_thesis: verum
end;

theorem Th3: :: ANALOAF:3
for V being RealLinearSpace
for u, v being VECTOR of V
for a being Real holds a * (u - v) = - (a * (v - u))
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V
for a being Real holds a * (u - v) = - (a * (v - u))
let u, v be VECTOR of V; ::_thesis: for a being Real holds a * (u - v) = - (a * (v - u))
let a be Real; ::_thesis: a * (u - v) = - (a * (v - u))
(a * (v - u)) + (a * (u - v)) = (a * (v - u)) + (a * (- (v - u))) by RLVECT_1:33
.= (a * (v - u)) - (a * (v - u)) by RLVECT_1:25
.= 0. V by RLVECT_1:15 ;
hence  a * (u - v) = - (a * (v - u)) by RLVECT_1:def_10; ::_thesis: verum
end;

theorem Th4: :: ANALOAF:4
for V being RealLinearSpace
for u, v being VECTOR of V
for a, b being Real holds (a - b) * (u - v) = (b - a) * (v - u)
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V
for a, b being Real holds (a - b) * (u - v) = (b - a) * (v - u)
let u, v be VECTOR of V; ::_thesis: for a, b being Real holds (a - b) * (u - v) = (b - a) * (v - u)
let a, b be Real; ::_thesis: (a - b) * (u - v) = (b - a) * (v - u)
thus (a - b) * (u - v) = (- (b - a)) * (- (v - u)) by RLVECT_1:33
.= (b - a) * (v - u) by RLVECT_1:26 ; ::_thesis: verum
end;

theorem Th5: :: ANALOAF:5
for V being RealLinearSpace
for u, v being VECTOR of V
for a being Real st a <> 0 & a * u = v holds
u = (a ") * v
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V
for a being Real st a <> 0 & a * u = v holds
u = (a ") * v
let u, v be VECTOR of V; ::_thesis: for a being Real st a <> 0 & a * u = v holds
u = (a ") * v
let a be Real; ::_thesis: ( a <> 0 & a * u = v implies u = (a ") * v )
assume that
A1: a <> 0 and
A2: a * u = v ; ::_thesis: u = (a ") * v
thus u = 1 * u by RLVECT_1:def_8
.= ((a ") * a) * u by A1, XCMPLX_0:def_7
.= (a ") * v by A2, RLVECT_1:def_7 ; ::_thesis: verum
end;

theorem Th6: :: ANALOAF:6
for V being RealLinearSpace
for u, v being VECTOR of V
for a being Real holds
( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) )
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V
for a being Real holds
( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) )
let u, v be VECTOR of V; ::_thesis: for a being Real holds
( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) )
let a be Real; ::_thesis: ( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) )
now__::_thesis:_(_a_<>_0_&_u_=_(a_")_*_v_implies_v_=_a_*_u_)
assume  ( a <> 0 & u = (a ") * v ) ; ::_thesis: v = a * u
hence v = ((a ") ") * u by Th5, XCMPLX_1:202
.= a * u ;
::_thesis: verum
end;
hence  ( ( a <> 0 & a * u = v implies u = (a ") * v ) & ( a <> 0 & u = (a ") * v implies a * u = v ) ) by Th5; ::_thesis: verum
end;

theorem Th7: :: ANALOAF:7
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v // w,y & u <> v & w <> y holds
ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V st u,v // w,y & u <> v & w <> y holds
ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b )
let u, v, w, y be VECTOR of V; ::_thesis: ( u,v // w,y & u <> v & w <> y implies ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b ) )
assume that
A1: u,v // w,y and
A2: ( u <> v & w <> y ) ; ::_thesis: ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b )
 ( u = v or w = y or ex a, b being Real st
( 0 < a & 0 < b & a * (v - u) = b * (y - w) ) ) by A1, Def1;
hence  ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b ) by A2; ::_thesis: verum
end;

theorem Th8: :: ANALOAF:8
for V being RealLinearSpace
for u, v being VECTOR of V holds u,v // u,v
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V holds u,v // u,v
let u, v be VECTOR of V; ::_thesis: u,v // u,v
 1 * (v - u) = 1 * (v - u) ;
hence  u,v // u,v by Def1; ::_thesis: verum
end;

theorem :: ANALOAF:9
for V being RealLinearSpace
for u, v, w being VECTOR of V holds
( u,v // w,w & u,u // v,w ) by Def1;

theorem Th10: :: ANALOAF:10
for V being RealLinearSpace
for u, v being VECTOR of V st u,v // v,u holds
u = v
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V st u,v // v,u holds
u = v
let u, v be VECTOR of V; ::_thesis: ( u,v // v,u implies u = v )
assume A1: u,v // v,u ; ::_thesis: u = v
assume A2: u <> v ; ::_thesis: contradiction
then consider a, b being Real such that
A3: a * (v - u) = b * (u - v) and
A4: ( 0 < a & 0 < b ) by A1, Th7;
 a * (v - u) = - (b * (v - u)) by A3, Th3;
then  (b * (v - u)) + (a * (v - u)) = 0. V by RLVECT_1:5;
then  (b + a) * (v - u) = 0. V by RLVECT_1:def_6;
then  ( v - u = 0. V or b + a = 0 ) by RLVECT_1:11;
then  0. V = (- u) + v by A4, XREAL_1:34;
then v = - (- u) by RLVECT_1:def_10
.= u by RLVECT_1:17 ;
hence  contradiction by A2; ::_thesis: verum
end;

theorem Th11: :: ANALOAF:11
for V being RealLinearSpace
for p, q, u, v, w, y being VECTOR of V st p <> q & p,q // u,v & p,q // w,y holds
u,v // w,y
proof
let V be RealLinearSpace; ::_thesis: for p, q, u, v, w, y being VECTOR of V st p <> q & p,q // u,v & p,q // w,y holds
u,v // w,y
let p, q, u, v, w, y be VECTOR of V; ::_thesis: ( p <> q & p,q // u,v & p,q // w,y implies u,v // w,y )
assume that
A1: p <> q and
A2: p,q // u,v and
A3: p,q // w,y ; ::_thesis: u,v // w,y
now__::_thesis:_(_u_<>_v_&_w_<>_y_implies_u,v_//_w,y_)
assume that
A4: u <> v and
A5: w <> y ; ::_thesis: u,v // w,y
consider a, b being Real such that
A6: a * (q - p) = b * (v - u) and
A7: 0 < a and
A8: 0 < b by A1, A2, A4, Th7;
 0 < a " by A7, XREAL_1:122;
then A9: 0 < (a ") * b by A8, XREAL_1:129;
consider c, d being Real such that
A10: c * (q - p) = d * (y - w) and
A11: 0 < c and
A12: 0 < d by A1, A3, A5, Th7;
A13: q - p = (c ") * (d * (y - w)) by A10, A11, Th6
.= ((c ") * d) * (y - w) by RLVECT_1:def_7 ;
 0 < c " by A11, XREAL_1:122;
then A14: 0 < (c ") * d by A12, XREAL_1:129;
q - p = (a ") * (b * (v - u)) by A6, A7, Th6
.= ((a ") * b) * (v - u) by RLVECT_1:def_7 ;
hence  u,v // w,y by A13, A9, A14, Def1; ::_thesis: verum
end;
hence  u,v // w,y by Def1; ::_thesis: verum
end;

theorem Th12: :: ANALOAF:12
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v // w,y holds
( v,u // y,w & w,y // u,v )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V st u,v // w,y holds
( v,u // y,w & w,y // u,v )
let u, v, w, y be VECTOR of V; ::_thesis: ( u,v // w,y implies ( v,u // y,w & w,y // u,v ) )
assume A1: u,v // w,y ; ::_thesis: ( v,u // y,w & w,y // u,v )
now__::_thesis:_(_u_<>_v_&_w_<>_y_implies_(_v,u_//_y,w_&_w,y_//_u,v_)_)
assume  ( u <> v & w <> y ) ; ::_thesis: ( v,u // y,w & w,y // u,v )
then consider a, b being Real such that
A2: a * (v - u) = b * (y - w) and
A3: ( 0 < a & 0 < b ) by A1, Th7;
a * (u - v) = - (b * (y - w)) by A2, Th3
.= b * (w - y) by Th3 ;
hence  ( v,u // y,w & w,y // u,v ) by A2, A3, Def1; ::_thesis: verum
end;
hence  ( v,u // y,w & w,y // u,v ) by Def1; ::_thesis: verum
end;

theorem Th13: :: ANALOAF:13
for V being RealLinearSpace
for u, v, w being VECTOR of V st u,v // v,w holds
u,v // u,w
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being VECTOR of V st u,v // v,w holds
u,v // u,w
let u, v, w be VECTOR of V; ::_thesis: ( u,v // v,w implies u,v // u,w )
assume A1: u,v // v,w ; ::_thesis: u,v // u,w
now__::_thesis:_(_u_<>_v_&_v_<>_w_implies_u,v_//_u,w_)
assume  ( u <> v & v <> w ) ; ::_thesis: u,v // u,w
then consider a, b being Real such that
A2: a * (v - u) = b * (w - v) and
A3: 0 < a and
A4: 0 < b by A1, Th7;
A5: 0 < a + b by A3, A4, XREAL_1:34;
b * (w - u) = b * ((w - v) + (v - u)) by Th1
.= (a * (v - u)) + (b * (v - u)) by A2, RLVECT_1:def_5
.= (a + b) * (v - u) by RLVECT_1:def_6 ;
hence  u,v // u,w by A4, A5, Def1; ::_thesis: verum
end;
hence  u,v // u,w by Def1, Th8; ::_thesis: verum
end;

theorem Th14: :: ANALOAF:14
for V being RealLinearSpace
for u, v, w being VECTOR of V holds
( not u,v // u,w or u,v // v,w or u,w // w,v )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being VECTOR of V holds
( not u,v // u,w or u,v // v,w or u,w // w,v )
let u, v, w be VECTOR of V; ::_thesis: ( not u,v // u,w or u,v // v,w or u,w // w,v )
assume A1: u,v // u,w ; ::_thesis: ( u,v // v,w or u,w // w,v )
now__::_thesis:_(_u_<>_v_&_u_<>_w_&_not_u,v_//_v,w_implies_u,w_//_w,v_)
assume  ( u <> v & u <> w ) ; ::_thesis: ( u,v // v,w or u,w // w,v )
then consider a, b being Real such that
A2: a * (v - u) = b * (w - u) and
A3: 0 < a and
A4: 0 < b by A1, Th7;
w - v = (w - u) + (u - v) by Th1
.= (w - u) - (v - u) by RLVECT_1:33 ;
then A5: a * (w - v) = (a * (w - u)) - (b * (w - u)) by A2, RLVECT_1:34
.= (a - b) * (w - u) by RLVECT_1:35
.= (b - a) * (u - w) by Th4 ;
v - w = (v - u) + (u - w) by Th1
.= (v - u) - (w - u) by RLVECT_1:33 ;
then A6: b * (v - w) = (b * (v - u)) - (a * (v - u)) by A2, RLVECT_1:34
.= (b - a) * (v - u) by RLVECT_1:35
.= (a - b) * (u - v) by Th4 ;
A7: now__::_thesis:_(_not_a_<>_b_or_u,v_//_v,w_or_u,w_//_w,v_)
assume  a <> b ; ::_thesis: ( u,v // v,w or u,w // w,v )
then  ( 0 < a - b or 0 < b - a ) by XREAL_1:55;
then  ( v,u // w,v or w,u // v,w ) by A3, A4, A6, A5, Def1;
hence  ( u,v // v,w or u,w // w,v ) by Th12; ::_thesis: verum
end;
now__::_thesis:_(_not_a_=_b_or_u,v_//_v,w_or_u,w_//_w,v_)
assume  a = b ; ::_thesis: ( u,v // v,w or u,w // w,v )
then  (- u) + v = (- u) + w by A2, A3, RLVECT_1:36;
then  v = w by RLVECT_1:8;
hence  ( u,v // v,w or u,w // w,v ) by Def1; ::_thesis: verum
end;
hence  ( u,v // v,w or u,w // w,v ) by A7; ::_thesis: verum
end;
hence  ( u,v // v,w or u,w // w,v ) by Def1; ::_thesis: verum
end;

theorem Th15: :: ANALOAF:15
for V being RealLinearSpace
for v, u, y, w being VECTOR of V st v - u = y - w holds
u,v // w,y
proof
let V be RealLinearSpace; ::_thesis: for v, u, y, w being VECTOR of V st v - u = y - w holds
u,v // w,y
let v, u, y, w be VECTOR of V; ::_thesis: ( v - u = y - w implies u,v // w,y )
assume  v - u = y - w ; ::_thesis: u,v // w,y
then  1 * (v - u) = 1 * (y - w) ;
hence  u,v // w,y by Def1; ::_thesis: verum
end;

theorem Th16: :: ANALOAF:16
for V being RealLinearSpace
for y, v, w, u being VECTOR of V st y = (v + w) - u holds
( u,v // w,y & u,w // v,y )
proof
let V be RealLinearSpace; ::_thesis: for y, v, w, u being VECTOR of V st y = (v + w) - u holds
( u,v // w,y & u,w // v,y )
let y, v, w, u be VECTOR of V; ::_thesis: ( y = (v + w) - u implies ( u,v // w,y & u,w // v,y ) )
set y = (v + w) - u;
 ((v + w) - u) + u = v + w by RLSUB_2:61;
then  ( ((v + w) - u) - v = w - u & ((v + w) - u) - w = v - u ) by Th2;
hence  ( y = (v + w) - u implies ( u,v // w,y & u,w // v,y ) ) by Th15; ::_thesis: verum
end;

theorem Th17: :: ANALOAF:17
for V being RealLinearSpace st ex p, q being VECTOR of V st p <> q holds
for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
proof
let V be RealLinearSpace; ::_thesis: ( ex p, q being VECTOR of V st p <> q implies for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
given p, q being VECTOR of V such that A1: p <> q ; ::_thesis: for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
let u, v, w be VECTOR of V; ::_thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A2: now__::_thesis:_(_u_<>_w_implies_ex_y_being_M2(_the_carrier_of_V)_ex_y_being_VECTOR_of_V_st_
(_u,v_//_w,y_&_u,w_//_v,y_&_v_<>_y_)_)
assume A3: u <> w ; ::_thesis: ex y being M2( the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
take y = (v + w) - u; ::_thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A4: now__::_thesis:_not_v_=_y
assume  v = y ; ::_thesis: contradiction
then  v = v + (w - u) by RLVECT_1:def_3;
then  w - u = 0. V by RLVECT_1:9;
hence  contradiction by A3, RLVECT_1:21; ::_thesis: verum
end;
 ( u,v // w,y & u,w // v,y ) by Th16;
hence  ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_u_=_w_implies_ex_y_being_VECTOR_of_V_st_
(_u,v_//_w,y_&_u,w_//_v,y_&_v_<>_y_)_)
assume A5: u = w ; ::_thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A6: now__::_thesis:_(_u_=_v_implies_ex_y_being_VECTOR_of_V_st_
(_u,v_//_w,y_&_u,w_//_v,y_&_v_<>_y_)_)
assume  u = v ; ::_thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
then A7: ( u,v // w,p & u,v // w,q ) by Def1;
A8: ( v <> p or v <> q ) by A1;
 ( u,w // v,p & u,w // v,q ) by A5, Def1;
hence  ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A8, A7; ::_thesis: verum
end;
 ( u,v // w,u & u,w // v,u ) by A5, Def1;
hence  ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A6; ::_thesis: verum
end;
hence  ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A2; ::_thesis: verum
end;

theorem Th18: :: ANALOAF:18
for V being RealLinearSpace
for p, v, w, u being VECTOR of V st p <> v & v,p // p,w holds
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
proof
let V be RealLinearSpace; ::_thesis: for p, v, w, u being VECTOR of V st p <> v & v,p // p,w holds
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
let p, v, w, u be VECTOR of V; ::_thesis: ( p <> v & v,p // p,w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )
assume A1: ( p <> v & v,p // p,w ) ; ::_thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
A2: now__::_thesis:_(_p_<>_w_implies_ex_y_being_VECTOR_of_V_st_
(_u,p_//_p,y_&_u,v_//_w,y_)_)
assume  p <> w ; ::_thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
then consider a, b being Real such that
A3: a * (p - v) = b * (w - p) and
A4: 0 < a and
A5: 0 < b by A1, Th7;
set y = (((b ") * a) * (p - u)) + p;
A6: ((((b ") * a) * (p - u)) + p) - p = ((b ") * a) * (p - u) by RLSUB_2:61
.= (b ") * (a * (p - u)) by RLVECT_1:def_7 ;
A7: ((((b ") * a) * (p - u)) + p) - w = (((((b ") * a) * (p - u)) + p) - p) + (p - w) by Th1
.= (((((b ") * a) * (p - u)) + p) - p) - (w - p) by RLVECT_1:33 ;
v - u = (p - u) + (v - p) by Th1
.= (p - u) - (p - v) by RLVECT_1:33 ;
then a * (v - u) = (a * (p - u)) - (a * (p - v)) by RLVECT_1:34
.= (b * (((((b ") * a) * (p - u)) + p) - p)) - (b * (w - p)) by A3, A5, A6, Th6
.= b * (((((b ") * a) * (p - u)) + p) - w) by A7, RLVECT_1:34 ;
then A8: u,v // w,(((b ") * a) * (p - u)) + p by A4, A5, Def1;
 0 < b " by A5, XREAL_1:122;
then A9: 0 < (b ") * a by A4, XREAL_1:129;
1 * (((((b ") * a) * (p - u)) + p) - p) = ((((b ") * a) * (p - u)) + p) - p by RLVECT_1:def_8
.= ((b ") * a) * (p - u) by RLSUB_2:61 ;
then  u,p // p,(((b ") * a) * (p - u)) + p by A9, Def1;
hence  ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) by A8; ::_thesis: verum
end;
now__::_thesis:_(_p_=_w_implies_ex_y_being_VECTOR_of_V_st_
(_u,p_//_p,y_&_u,v_//_w,y_)_)
assume A10: p = w ; ::_thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
take y = p; ::_thesis: ( u,p // p,y & u,v // w,y )
thus  ( u,p // p,y & u,v // w,y ) by A10, Def1; ::_thesis: verum
end;
hence  ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) by A2; ::_thesis: verum
end;

theorem Th19: :: ANALOAF:19
for V being RealLinearSpace
for u, v being VECTOR of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) holds
( u <> v & u <> 0. V & v <> 0. V )
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) holds
( u <> v & u <> 0. V & v <> 0. V )
let u, v be VECTOR of V; ::_thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) implies ( u <> v & u <> 0. V & v <> 0. V ) )
assume A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; ::_thesis: ( u <> v & u <> 0. V & v <> 0. V )
thus  u <> v ::_thesis: ( u <> 0. V & v <> 0. V )
proof
assume  u = v ; ::_thesis: contradiction
then  u - v = 0. V by RLVECT_1:15;
then  (1 * u) + (- v) = 0. V by RLVECT_1:def_8;
then  (1 * u) + ((- 1) * v) = 0. V by RLVECT_1:16;
hence  contradiction by A1; ::_thesis: verum
end;
thus  u <> 0. V ::_thesis: v <> 0. V
proof
assume  u = 0. V ; ::_thesis: contradiction
then  1 * u = 0. V by RLVECT_1:10;
then  (1 * u) + (0. V) = 0. V by RLVECT_1:4;
then  (1 * u) + (0 * v) = 0. V by RLVECT_1:10;
hence  contradiction by A1; ::_thesis: verum
end;
thus  v <> 0. V ::_thesis: verum
proof
assume  v = 0. V ; ::_thesis: contradiction
then  1 * v = 0. V by RLVECT_1:10;
then  (0. V) + (1 * v) = 0. V by RLVECT_1:4;
then  (0 * u) + (1 * v) = 0. V by RLVECT_1:10;
hence  contradiction by A1; ::_thesis: verum
end;
end;

theorem Th20: :: ANALOAF:20
for V being RealLinearSpace st ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) holds
ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w )
proof
let V be RealLinearSpace; ::_thesis: ( ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w ) )
given u, v being VECTOR of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; ::_thesis: ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w )
A2: ( u <> 0. V & v <> 0. V ) by A1, Th19;
A3: not 0. V,u // v, 0. V
proof
A4: now__::_thesis:_for_a,_b_being_Real_holds_
(_not_0_<_a_or_not_0_<_b_or_not_a_*_(u_-_(0._V))_=_b_*_((0._V)_-_v)_)
given a, b being Real such that A5: 0 < a and
 0 < b and
A6: a * (u - (0. V)) = b * ((0. V) - v) ; ::_thesis: contradiction
 ( a * u = a * (u - (0. V)) & b * ((0. V) - v) = b * (- v) ) by RLVECT_1:13, RLVECT_1:14;
then  a * u = - (b * v) by A6, RLVECT_1:25;
then  (a * u) + (b * v) = 0. V by RLVECT_1:5;
hence  contradiction by A1, A5; ::_thesis: verum
end;
assume  0. V,u // v, 0. V ; ::_thesis: contradiction
hence  contradiction by A2, A4, Def1; ::_thesis: verum
end;
 not 0. V,u // 0. V,v
proof
A7: now__::_thesis:_for_a,_b_being_Real_holds_
(_not_0_<_a_or_not_0_<_b_or_not_a_*_(u_-_(0._V))_=_b_*_(v_-_(0._V))_)
given a, b being Real such that A8: 0 < a and
 0 < b and
A9: a * (u - (0. V)) = b * (v - (0. V)) ; ::_thesis: contradiction
 ( a * u = a * (u - (0. V)) & b * (v - (0. V)) = b * v ) by RLVECT_1:13;
then  0. V = (a * u) - (b * v) by A9, RLVECT_1:15
.= (a * u) + (b * (- v)) by RLVECT_1:25
.= (a * u) + ((- b) * v) by RLVECT_1:24 ;
hence  contradiction by A1, A8; ::_thesis: verum
end;
assume  0. V,u // 0. V,v ; ::_thesis: contradiction
hence  contradiction by A2, A7, Def1; ::_thesis: verum
end;
hence  ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w ) by A3; ::_thesis: verum
end;

Lm1:  for V being RealLinearSpace
for v, u, w, y being VECTOR of V
for a, b being Real st a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y holds
u,v // y,w
proof
let V be RealLinearSpace; ::_thesis: for v, u, w, y being VECTOR of V
for a, b being Real st a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y holds
u,v // y,w
let v, u, w, y be VECTOR of V; ::_thesis: for a, b being Real st a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y holds
u,v // y,w
let a, b be Real; ::_thesis: ( a * (v - u) = b * (w - y) & ( a <> 0 or b <> 0 ) & not u,v // w,y implies u,v // y,w )
assume that
A1: a * (v - u) = b * (w - y) and
A2: ( a <> 0 or b <> 0 ) ; ::_thesis: ( u,v // w,y or u,v // y,w )
A3: now__::_thesis:_(_b_=_0_implies_u,v_//_w,y_)
assume A4: b = 0 ; ::_thesis: u,v // w,y
then  0. V = a * (v - u) by A1, RLVECT_1:10;
then  v - u = 0. V by A2, A4, RLVECT_1:11;
then  u = v by RLVECT_1:21;
hence  u,v // w,y by Def1; ::_thesis: verum
end;
A5: now__::_thesis:_(_a_<>_0_&_b_<>_0_&_not_u,v_//_w,y_implies_u,v_//_y,w_)
A6: now__::_thesis:_(_0_<_a_&_b_<_0_implies_u,v_//_w,y_)
A7: a * (v - u) = - (- (b * (w - y))) by A1, RLVECT_1:17
.= - (b * (- (w - y))) by RLVECT_1:25
.= - (b * (y - w)) by RLVECT_1:33
.= b * (- (y - w)) by RLVECT_1:25
.= (- b) * (y - w) by RLVECT_1:24 ;
assume that
A8: 0 < a and
A9: b < 0 ; ::_thesis: u,v // w,y
 0 < - b by A9, XREAL_1:58;
hence  u,v // w,y by A8, A7, Def1; ::_thesis: verum
end;
A10: now__::_thesis:_(_a_<_0_&_0_<_b_implies_u,v_//_w,y_)
A11: (- a) * (v - u) = a * (- (v - u)) by RLVECT_1:24
.= - (b * (w - y)) by A1, RLVECT_1:25
.= b * (- (w - y)) by RLVECT_1:25
.= b * (y - w) by RLVECT_1:33 ;
assume that
A12: a < 0 and
A13: 0 < b ; ::_thesis: u,v // w,y
 0 < - a by A12, XREAL_1:58;
hence  u,v // w,y by A13, A11, Def1; ::_thesis: verum
end;
A14: now__::_thesis:_(_a_<_0_&_b_<_0_implies_u,v_//_y,w_)
assume  ( a < 0 & b < 0 ) ; ::_thesis: u,v // y,w
then A15: ( 0 < - a & 0 < - b ) by XREAL_1:58;
(- a) * (v - u) = a * (- (v - u)) by RLVECT_1:24
.= - (b * (w - y)) by A1, RLVECT_1:25
.= b * (- (w - y)) by RLVECT_1:25
.= (- b) * (w - y) by RLVECT_1:24 ;
hence  u,v // y,w by A15, Def1; ::_thesis: verum
end;
assume  ( a <> 0 & b <> 0 ) ; ::_thesis: ( u,v // w,y or u,v // y,w )
hence  ( u,v // w,y or u,v // y,w ) by A1, A14, A10, A6, Def1; ::_thesis: verum
end;
now__::_thesis:_(_a_=_0_implies_u,v_//_w,y_)
assume A16: a = 0 ; ::_thesis: u,v // w,y
then  0. V = b * (w - y) by A1, RLVECT_1:10;
then  w - y = 0. V by A2, A16, RLVECT_1:11;
then  w = y by RLVECT_1:21;
hence  u,v // w,y by Def1; ::_thesis: verum
end;
hence  ( u,v // w,y or u,v // y,w ) by A3, A5; ::_thesis: verum
end;

theorem Th21: :: ANALOAF:21
for V being RealLinearSpace st ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w holds
for u, v, w, y being VECTOR of V st not u,v // w,y & not u,v // y,w holds
ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
proof
let V be RealLinearSpace; ::_thesis: ( ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w implies for u, v, w, y being VECTOR of V st not u,v // w,y & not u,v // y,w holds
ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) )
given p, q being VECTOR of V such that A1: for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w ; ::_thesis: for u, v, w, y being VECTOR of V st not u,v // w,y & not u,v // y,w holds
ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
let u, v, w, y be VECTOR of V; ::_thesis: ( not u,v // w,y & not u,v // y,w implies ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) )
assume that
A2: not u,v // w,y and
A3: not u,v // y,w ; ::_thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
consider r1, s1 being Real such that
A4: (r1 * p) + (s1 * q) = v - u by A1;
consider r2, s2 being Real such that
A5: (r2 * p) + (s2 * q) = y - w by A1;
set r = (r1 * s2) - (r2 * s1);
A6: now__::_thesis:_not_(r1_*_s2)_-_(r2_*_s1)_=_0
assume A7: (r1 * s2) - (r2 * s1) = 0 ; ::_thesis: contradiction
A8: now__::_thesis:_(_r1_<>_0_implies_not_r2_=_0_)
assume that
A9: r1 <> 0 and
A10: r2 = 0 ; ::_thesis: contradiction
 s2 <> 0
proof
assume  s2 = 0 ; ::_thesis: contradiction
then y - w = (0. V) + (0 * q) by A5, A10, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then  y = w by RLVECT_1:21;
hence  contradiction by A2, Def1; ::_thesis: verum
end;
hence  contradiction by A7, A9, A10, XCMPLX_1:6; ::_thesis: verum
end;
A11: now__::_thesis:_not_r1_=_0
assume A12: r1 = 0 ; ::_thesis: contradiction
A13: s1 <> 0
proof
assume  s1 = 0 ; ::_thesis: contradiction
then v - u = (0. V) + (0 * q) by A4, A12, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then  u = v by RLVECT_1:21;
hence  contradiction by A2, Def1; ::_thesis: verum
end;
then A14: r2 = 0 by A7, A12, XCMPLX_1:6;
A15: s2 <> 0
proof
assume  s2 = 0 ; ::_thesis: contradiction
then y - w = (0. V) + (0 * q) by A5, A14, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then  y = w by RLVECT_1:21;
hence  contradiction by A2, Def1; ::_thesis: verum
end;
y - w = (0. V) + (s2 * q) by A5, A14, RLVECT_1:10
.= s2 * q by RLVECT_1:4 ;
then A16: (s2 ") * (y - w) = ((s2 ") * s2) * q by RLVECT_1:def_7
.= 1 * q by A15, XCMPLX_0:def_7
.= q by RLVECT_1:def_8 ;
v - u = (0. V) + (s1 * q) by A4, A12, RLVECT_1:10
.= s1 * q by RLVECT_1:4 ;
then A17: (s1 ") * (v - u) = ((s1 ") * s1) * q by RLVECT_1:def_7
.= 1 * q by A13, XCMPLX_0:def_7
.= q by RLVECT_1:def_8 ;
 s1 " <> 0 by A13, XCMPLX_1:202;
hence  contradiction by A2, A3, A17, A16, Lm1; ::_thesis: verum
end;
A18: now__::_thesis:_(_r1_<>_0_&_r2_<>_0_implies_not_s1_=_0_)
assume that
A19: r1 <> 0 and
A20: r2 <> 0 and
A21: s1 = 0 ; ::_thesis: contradiction
v - u = (r1 * p) + (0. V) by A4, A21, RLVECT_1:10
.= r1 * p by RLVECT_1:4 ;
then A22: (r1 ") * (v - u) = ((r1 ") * r1) * p by RLVECT_1:def_7
.= 1 * p by A19, XCMPLX_0:def_7
.= p by RLVECT_1:def_8 ;
 s2 = 0 by A7, A19, A21, XCMPLX_1:6;
then y - w = (r2 * p) + (0. V) by A5, RLVECT_1:10
.= r2 * p by RLVECT_1:4 ;
then A23: (r2 ") * (y - w) = ((r2 ") * r2) * p by RLVECT_1:def_7
.= 1 * p by A20, XCMPLX_0:def_7
.= p by RLVECT_1:def_8 ;
 r1 " <> 0 by A19, XCMPLX_1:202;
hence  contradiction by A2, A3, A22, A23, Lm1; ::_thesis: verum
end;
now__::_thesis:_(_r1_<>_0_&_r2_<>_0_&_s1_<>_0_implies_not_s2_<>_0_)
assume that
A24: r1 <> 0 and
 r2 <> 0 and
 s1 <> 0 and
 s2 <> 0 ; ::_thesis: contradiction
r2 * (v - u) = (r2 * (r1 * p)) + (r2 * (s1 * q)) by A4, RLVECT_1:def_5
.= ((r2 * r1) * p) + (r2 * (s1 * q)) by RLVECT_1:def_7
.= ((r1 * r2) * p) + ((r1 * s2) * q) by A7, RLVECT_1:def_7
.= (r1 * (r2 * p)) + ((r1 * s2) * q) by RLVECT_1:def_7
.= (r1 * (r2 * p)) + (r1 * (s2 * q)) by RLVECT_1:def_7
.= r1 * (y - w) by A5, RLVECT_1:def_5 ;
hence  contradiction by A2, A3, A24, Lm1; ::_thesis: verum
end;
hence  contradiction by A7, A11, A8, A18, XCMPLX_1:6; ::_thesis: verum
end;
consider r3, s3 being Real such that
A25: (r3 * p) + (s3 * q) = u - w by A1;
set a = (r2 * s3) - (r3 * s2);
set b = (r1 * s3) - (r3 * s1);
A26: ((r1 * s3) - (r3 * s1)) * r2 = (r1 * ((r2 * s3) - (r3 * s2))) + (r3 * ((r1 * s2) - (r2 * s1))) ;
set z = u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u));
A27: ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - u) = (((r1 * s2) - (r2 * s1)) * (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:34
.= ((((r1 * s2) - (r2 * s1)) * u) + (((r1 * s2) - (r2 * s1)) * (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:def_5
.= ((((r1 * s2) - (r2 * s1)) * u) + ((((r1 * s2) - (r2 * s1)) * ((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2)))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:def_7
.= ((((r1 * s2) - (r2 * s1)) * u) + (((((r1 * s2) - (r2 * s1)) * (((r1 * s2) - (r2 * s1)) ")) * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u)
.= ((((r1 * s2) - (r2 * s1)) * u) + ((1 * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u) by A6, XCMPLX_0:def_7
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + ((((r1 * s2) - (r2 * s1)) * u) - (((r1 * s2) - (r2 * s1)) * u)) by RLVECT_1:def_3
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + (0. V) by RLVECT_1:15
.= ((r2 * s3) - (r3 * s2)) * (v - u) by RLVECT_1:4 ;
A28: ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - w) = (((r1 * s2) - (r2 * s1)) * (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:34
.= ((((r1 * s2) - (r2 * s1)) * u) + (((r1 * s2) - (r2 * s1)) * (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:def_5
.= ((((r1 * s2) - (r2 * s1)) * u) + ((((r1 * s2) - (r2 * s1)) * ((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2)))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:def_7
.= ((((r1 * s2) - (r2 * s1)) * u) + (((((r1 * s2) - (r2 * s1)) * (((r1 * s2) - (r2 * s1)) ")) * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w)
.= ((((r1 * s2) - (r2 * s1)) * u) + ((1 * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w) by A6, XCMPLX_0:def_7
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + ((((r1 * s2) - (r2 * s1)) * u) - (((r1 * s2) - (r2 * s1)) * w)) by RLVECT_1:def_3
.= (((r2 * s3) - (r3 * s2)) * ((r1 * p) + (s1 * q))) + (((r1 * s2) - (r2 * s1)) * ((r3 * p) + (s3 * q))) by A4, A25, RLVECT_1:34
.= ((((r2 * s3) - (r3 * s2)) * (r1 * p)) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + (((r1 * s2) - (r2 * s1)) * ((r3 * p) + (s3 * q))) by RLVECT_1:def_5
.= ((((r2 * s3) - (r3 * s2)) * (r1 * p)) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def_5
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def_7
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def_7
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + (((((r1 * s2) - (r2 * s1)) * r3) * p) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def_7
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + (((((r1 * s2) - (r2 * s1)) * s3) * q) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def_7
.= ((((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + ((((r1 * s2) - (r2 * s1)) * r3) * p) by RLVECT_1:def_3
.= ((((((r2 * s3) - (r3 * s2)) * s1) * q) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + ((((r2 * s3) - (r3 * s2)) * r1) * p)) + ((((r1 * s2) - (r2 * s1)) * r3) * p) by RLVECT_1:def_3
.= (((((r2 * s3) - (r3 * s2)) * s1) * q) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def_3
.= (((((r2 * s3) - (r3 * s2)) * s1) + (((r1 * s2) - (r2 * s1)) * s3)) * q) + (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def_6
.= ((((r1 * s3) - (r3 * s1)) * s2) * q) + ((((r1 * s3) - (r3 * s1)) * r2) * p) by A26, RLVECT_1:def_6
.= (((r1 * s3) - (r3 * s1)) * (s2 * q)) + ((((r1 * s3) - (r3 * s1)) * r2) * p) by RLVECT_1:def_7
.= (((r1 * s3) - (r3 * s1)) * (s2 * q)) + (((r1 * s3) - (r3 * s1)) * (r2 * p)) by RLVECT_1:def_7
.= ((r1 * s3) - (r3 * s1)) * (y - w) by A5, RLVECT_1:def_5 ;
A29: now__::_thesis:_(_(r2_*_s3)_-_(r3_*_s2)_=_0_&_(r1_*_s3)_-_(r3_*_s1)_<>_0_implies_ex_z_being_VECTOR_of_V_st_
(_(_u,v_//_u,z_or_u,v_//_z,u_)_&_(_w,y_//_w,z_or_w,y_//_z,w_)_)_)
assume that
A30: (r2 * s3) - (r3 * s2) = 0 and
A31: (r1 * s3) - (r3 * s1) <> 0 ; ::_thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
 ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - u) = 0. V by A27, A30, RLVECT_1:10;
then  (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - u = 0. V by A6, RLVECT_1:11;
then  u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) = u by RLVECT_1:21;
then A32: u,v // u,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) by Def1;
 ( w,y // w,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or w,y // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),w ) by A28, A31, Lm1;
hence  ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A32; ::_thesis: verum
end;
A33: ((r1 * s3) - (r3 * s1)) * s2 = (s1 * ((r2 * s3) - (r3 * s2))) + (s3 * ((r1 * s2) - (r2 * s1))) ;
A34: now__::_thesis:_(_(r2_*_s3)_-_(r3_*_s2)_=_0_&_(r1_*_s3)_-_(r3_*_s1)_=_0_implies_ex_z_being_VECTOR_of_V_st_
(_(_u,v_//_u,z_or_u,v_//_z,u_)_&_(_w,y_//_w,z_or_w,y_//_z,w_)_)_)
assume  ( (r2 * s3) - (r3 * s2) = 0 & (r1 * s3) - (r3 * s1) = 0 ) ; ::_thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
then  ( r3 = 0 & s3 = 0 ) by A6, A26, A33, XCMPLX_1:6;
then  (0. V) + (0 * q) = u - w by A25, RLVECT_1:10;
then  (0. V) + (0. V) = u - w by RLVECT_1:10;
then  0. V = u - w by RLVECT_1:4;
then  u = w by RLVECT_1:21;
then A35: w,y // w,u by Def1;
 u,v // u,u by Def1;
hence  ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A35; ::_thesis: verum
end;
A36: now__::_thesis:_(_(r2_*_s3)_-_(r3_*_s2)_<>_0_&_(r1_*_s3)_-_(r3_*_s1)_=_0_implies_ex_z_being_VECTOR_of_V_st_
(_(_u,v_//_u,z_or_u,v_//_z,u_)_&_(_w,y_//_w,z_or_w,y_//_z,w_)_)_)
assume that
A37: (r2 * s3) - (r3 * s2) <> 0 and
A38: (r1 * s3) - (r3 * s1) = 0 ; ::_thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
 ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - w) = 0. V by A28, A38, RLVECT_1:10;
then  (u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u))) - w = 0. V by A6, RLVECT_1:11;
then  u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) = w by RLVECT_1:21;
then A39: w,y // w,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) by Def1;
 ( u,v // u,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or u,v // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),u ) by A27, A37, Lm1;
hence  ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A39; ::_thesis: verum
end;
now__::_thesis:_(_(r2_*_s3)_-_(r3_*_s2)_<>_0_&_(r1_*_s3)_-_(r3_*_s1)_<>_0_implies_ex_z_being_VECTOR_of_V_st_
(_(_u,v_//_u,z_or_u,v_//_z,u_)_&_(_w,y_//_w,z_or_w,y_//_z,w_)_)_)
assume that
A40: (r2 * s3) - (r3 * s2) <> 0 and
A41: (r1 * s3) - (r3 * s1) <> 0 ; ::_thesis: ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) )
A42: ( w,y // w,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or w,y // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),w ) by A28, A41, Lm1;
 ( u,v // u,u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)) or u,v // u + (((((r1 * s2) - (r2 * s1)) ") * ((r2 * s3) - (r3 * s2))) * (v - u)),u ) by A27, A40, Lm1;
hence  ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A42; ::_thesis: verum
end;
hence  ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A34, A29, A36; ::_thesis: verum
end;

definition
attrc1 is strict ;
struct AffinStruct  ->  1-sorted ;
aggrAffinStruct(# carrier, CONGR #) ->  AffinStruct ;
sel CONGR c1 ->  Relation of [: the carrier of c1, the carrier of c1:];
end;

registration
cluster non trivial strict for AffinStruct ;
existence
 ex b1 being AffinStruct st
( not b1 is trivial & b1 is strict )
proof
set A = the non trivial set ;
set R = the Relation of [: the non trivial set , the non trivial set :];
take  AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) ; ::_thesis: ( not AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is trivial & AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is strict )
thus  ( not AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is trivial & AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is strict ) ; ::_thesis: verum
end;
end;


definition
let AS be non empty AffinStruct ;
let a, b, c, d be Element of AS;
preda,b // c,d means :Def2: :: ANALOAF:def 2
[[a,b],[c,d]] in the CONGR of AS;
end;

:: deftheorem Def2 defines // ANALOAF:def_2_:_
 for AS being non empty AffinStruct
for a, b, c, d being Element of AS holds
( a,b // c,d iff [[a,b],[c,d]] in the CONGR of AS );

definition
let V be RealLinearSpace;
func DirPar V ->  Relation of [: the carrier of V, the carrier of V:] means :Def3: :: ANALOAF:def 3
 for x, z being set holds
( [x,z] in it iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) );
existence
 ex b1 being Relation of [: the carrier of V, the carrier of V:] st
for x, z being set holds
( [x,z] in b1 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) )
proof
defpred S1[ set , set ] means  ex u, v, w, y being VECTOR of V st
( $1 = [u,v] & $2 = [w,y] & u,v // w,y );
set VV = [: the carrier of V, the carrier of V:];
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 x, z being set holds
( [x,z] in P iff ( x in [: the carrier of V, the carrier of V:] & z in [: the carrier of V, the carrier of V:] & S1[x,z] ) ) from RELSET_1:sch_1();
take  P ; ::_thesis: for x, z being set holds
( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) )
let x, z be set ; ::_thesis: ( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) )
thus  ( [x,z] in P implies ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) by A1; ::_thesis: ( ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) implies [x,z] in P )
assume  ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ; ::_thesis: [x,z] in P
hence  [x,z] in P by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of [: the carrier of V, the carrier of V:] st ( for x, z being set holds
( [x,z] in b1 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) & ( for x, z being set holds
( [x,z] in b2 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) holds
b1 = b2
proof
let P, Q be Relation of [: the carrier of V, the carrier of V:]; ::_thesis: ( ( for x, z being set holds
( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) & ( for x, z being set holds
( [x,z] in Q iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) implies P = Q )
assume that
A2: for x, z being set holds
( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) and
A3: for x, z being set holds
( [x,z] in Q iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ; ::_thesis: P = Q
 for x, z being set holds
( [x,z] in P iff [x,z] in Q )
proof
let x, z be set ; ::_thesis: ( [x,z] in P iff [x,z] in Q )
 ( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) by A2;
hence  ( [x,z] in P iff [x,z] in Q ) by A3; ::_thesis: verum
end;
hence  P = Q by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines DirPar ANALOAF:def_3_:_
 for V being RealLinearSpace
for b2 being Relation of [: the carrier of V, the carrier of V:] holds
( b2 = DirPar V iff for x, z being set holds
( [x,z] in b2 iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) );

theorem Th22: :: ANALOAF:22
for V being RealLinearSpace
for u, v, w, y being VECTOR of V holds
( [[u,v],[w,y]] in DirPar V iff u,v // w,y )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V holds
( [[u,v],[w,y]] in DirPar V iff u,v // w,y )
let u, v, w, y be VECTOR of V; ::_thesis: ( [[u,v],[w,y]] in DirPar V iff u,v // w,y )
thus  ( [[u,v],[w,y]] in DirPar V implies u,v // w,y ) ::_thesis: ( u,v // w,y implies [[u,v],[w,y]] in DirPar V )
proof
assume  [[u,v],[w,y]] in DirPar V ; ::_thesis: u,v // w,y
then consider u9, v9, w9, y9 being VECTOR of V such that
A1: [u,v] = [u9,v9] and
A2: [w,y] = [w9,y9] and
A3: u9,v9 // w9,y9 by Def3;
A4: w = w9 by A2, XTUPLE_0:1;
 ( u = u9 & v = v9 ) by A1, XTUPLE_0:1;
hence  u,v // w,y by A2, A3, A4, XTUPLE_0:1; ::_thesis: verum
end;
thus  ( u,v // w,y implies [[u,v],[w,y]] in DirPar V ) by Def3; ::_thesis: verum
end;

definition
let V be RealLinearSpace;
func OASpace V ->  strict AffinStruct  equals :: ANALOAF:def 4
 AffinStruct(# the carrier of V,(DirPar V) #);
correctness
coherence
AffinStruct(# the carrier of V,(DirPar V) #) is strict AffinStruct ;
;
end;

:: deftheorem  defines OASpace ANALOAF:def_4_:_
 for V being RealLinearSpace holds OASpace V = AffinStruct(# the carrier of V,(DirPar V) #);

registration
let V be RealLinearSpace;
cluster OASpace V ->  non empty strict ;
coherence
 not OASpace V is empty ;
end;

theorem Th23: :: ANALOAF:23
for V being RealLinearSpace st ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) holds
( ex a, b being Element of (OASpace V) st a <> b & ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ) )
proof
let V be RealLinearSpace; ::_thesis: ( ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies ( ex a, b being Element of (OASpace V) st a <> b & ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ) ) )
given u, v being VECTOR of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; ::_thesis: ( ex a, b being Element of (OASpace V) st a <> b & ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ) )
set S = OASpace V;
A2: u <> v by A1, Th19;
hence  ex a, b being Element of (OASpace V) st a <> b ; ::_thesis: ( ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ) )
thus  for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ::_thesis: ( ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ) )
proof
let a, b, c, d, p, q, r, s be Element of (OASpace V); ::_thesis: ( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q, r9 = r, s9 = s as Element of V ;
 a9,b9 // c9,c9 by Def1;
hence  [[a,b],[c,c]] in the CONGR of (OASpace V) by Def3; :: according to ANALOAF:def_2 ::_thesis: ( ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) )
thus  ( a,b // b,a implies a = b ) ::_thesis: ( ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) )
proof
assume  [[a,b],[b,a]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def_2 ::_thesis: a = b
then  a9,b9 // b9,a9 by Th22;
hence  a = b by Th10; ::_thesis: verum
end;
thus  ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) ::_thesis: ( ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) )
proof
assume that
A3: a <> b and
A4: ( [[a,b],[p,q]] in the CONGR of (OASpace V) & [[a,b],[r,s]] in the CONGR of (OASpace V) ) ; :: according to ANALOAF:def_2 ::_thesis: p,q // r,s
 ( a9,b9 // p9,q9 & a9,b9 // r9,s9 ) by A4, Th22;
then  p9,q9 // r9,s9 by A3, Th11;
then  [[p,q],[r,s]] in the CONGR of (OASpace V) by Th22;
hence  p,q // r,s by Def2; ::_thesis: verum
end;
thus  ( a,b // c,d implies b,a // d,c ) ::_thesis: ( ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) )
proof
assume  [[a,b],[c,d]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def_2 ::_thesis: b,a // d,c
then  a9,b9 // c9,d9 by Th22;
then  b9,a9 // d9,c9 by Th12;
then  [[b,a],[d,c]] in the CONGR of (OASpace V) by Th22;
hence  b,a // d,c by Def2; ::_thesis: verum
end;
thus  ( a,b // b,c implies a,b // a,c ) ::_thesis: ( not a,b // a,c or a,b // b,c or a,c // c,b )
proof
assume  [[a,b],[b,c]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def_2 ::_thesis: a,b // a,c
then  a9,b9 // b9,c9 by Th22;
then  a9,b9 // a9,c9 by Th13;
then  [[a,b],[a,c]] in the CONGR of (OASpace V) by Th22;
hence  a,b // a,c by Def2; ::_thesis: verum
end;
thus  ( not a,b // a,c or a,b // b,c or a,c // c,b ) ::_thesis: verum
proof
assume  [[a,b],[a,c]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def_2 ::_thesis: ( a,b // b,c or a,c // c,b )
then  a9,b9 // a9,c9 by Th22;
then  ( a9,b9 // b9,c9 or a9,c9 // c9,b9 ) by Th14;
then  ( [[a,b],[b,c]] in the CONGR of (OASpace V) or [[a,c],[c,b]] in the CONGR of (OASpace V) ) by Th22;
hence  ( a,b // b,c or a,c // c,b ) by Def2; ::_thesis: verum
end;
end;
thus  ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) ::_thesis: ( ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ) )
proof
consider a9, b9, c9, d9 being VECTOR of V such that
A5: not a9,b9 // c9,d9 and
A6: not a9,b9 // d9,c9 by A1, Th20;
reconsider a = a9, b = b9, c = c9, d = d9 as Element of (OASpace V) ;
 not [[a,b],[d,c]] in the CONGR of (OASpace V) by A6, Th22;
then A7: not a,b // d,c by Def2;
 not [[a,b],[c,d]] in the CONGR of (OASpace V) by A5, Th22;
then  not a,b // c,d by Def2;
hence  ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) by A7; ::_thesis: verum
end;
thus  for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ::_thesis: for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d )
proof
let a, b, c be Element of (OASpace V); ::_thesis: ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d )
reconsider a9 = a, b9 = b, c9 = c as Element of V ;
consider d9 being VECTOR of V such that
A8: a9,b9 // c9,d9 and
A9: a9,c9 // b9,d9 and
A10: b9 <> d9 by A2, Th17;
reconsider d = d9 as Element of (OASpace V) ;
 [[a,c],[b,d]] in the CONGR of (OASpace V) by A9, Th22;
then A11: a,c // b,d by Def2;
 [[a,b],[c,d]] in the CONGR of (OASpace V) by A8, Th22;
then  a,b // c,d by Def2;
hence  ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) by A10, A11; ::_thesis: verum
end;
thus  for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ::_thesis: verum
proof
let p, a, b, c be Element of (OASpace V); ::_thesis: ( p <> b & b,p // p,c implies ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) )
assume that
A12: p <> b and
A13: [[b,p],[p,c]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def_2 ::_thesis: ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d )
reconsider p9 = p, a9 = a, b9 = b, c9 = c as Element of V ;
 b9,p9 // p9,c9 by A13, Th22;
then consider d9 being VECTOR of V such that
A14: a9,p9 // p9,d9 and
A15: a9,b9 // c9,d9 by A12, Th18;
reconsider d = d9 as Element of (OASpace V) ;
 [[a,b],[c,d]] in the CONGR of (OASpace V) by A15, Th22;
then A16: a,b // c,d by Def2;
 [[a,p],[p,d]] in the CONGR of (OASpace V) by A14, Th22;
then  a,p // p,d by Def2;
hence  ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) by A16; ::_thesis: verum
end;
end;

theorem Th24: :: ANALOAF:24
for V being RealLinearSpace st ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w holds
for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
proof
let V be RealLinearSpace; ::_thesis: ( ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w implies for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )
assume A1: ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w ; ::_thesis: for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
set S = OASpace V;
let a, b, c, d be Element of (OASpace V); ::_thesis: ( not a,b // c,d & not a,b // d,c implies ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of V ;
assume  ( not [[a,b],[c,d]] in the CONGR of (OASpace V) & not [[a,b],[d,c]] in the CONGR of (OASpace V) ) ; :: according to ANALOAF:def_2 ::_thesis: ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
then  ( not a9,b9 // c9,d9 & not a9,b9 // d9,c9 ) by Th22;
then consider t9 being VECTOR of V such that
A2: ( a9,b9 // a9,t9 or a9,b9 // t9,a9 ) and
A3: ( c9,d9 // c9,t9 or c9,d9 // t9,c9 ) by A1, Th21;
reconsider t = t9 as Element of (OASpace V) ;
 ( [[c,d],[c,t]] in the CONGR of (OASpace V) or [[c,d],[t,c]] in the CONGR of (OASpace V) ) by A3, Th22;
then A4: ( c,d // c,t or c,d // t,c ) by Def2;
 ( [[a,b],[a,t]] in the CONGR of (OASpace V) or [[a,b],[t,a]] in the CONGR of (OASpace V) ) by A2, Th22;
then  ( a,b // a,t or a,b // t,a ) by Def2;
hence  ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) by A4; ::_thesis: verum
end;

definition
let IT be non empty AffinStruct ;
attrIT is OAffinSpace-like  means :Def5: :: ANALOAF:def 5
( ( for a, b, c, d, p, q, r, s being Element of IT holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of IT st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of IT ex d being Element of IT st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of IT st p <> b & b,p // p,c holds
ex d being Element of IT st
( a,p // p,d & a,b // c,d ) ) );
end;

:: deftheorem Def5 defines OAffinSpace-like ANALOAF:def_5_:_
 for IT being non empty AffinStruct holds
( IT is OAffinSpace-like iff ( ( for a, b, c, d, p, q, r, s being Element of IT holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of IT st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of IT ex d being Element of IT st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of IT st p <> b & b,p // p,c holds
ex d being Element of IT st
( a,p // p,d & a,b // c,d ) ) ) );

registration
cluster non empty non trivial strict OAffinSpace-like for AffinStruct ;
existence
 ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is OAffinSpace-like )
proof
consider V being RealLinearSpace, u, v being VECTOR of V such that
A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) and
 for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) by FUNCSDOM:23;
A2: ( ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) ) by A1, Th23;
A3: for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) by A1, Th23;
 ( ex a, b being Element of (OASpace V) st a <> b & ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) ) by A1, Th23;
then  ( not OASpace V is trivial & OASpace V is OAffinSpace-like ) by A2, A3, Def5, STRUCT_0:def_10;
hence  ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is OAffinSpace-like ) ; ::_thesis: verum
end;
end;

definition
mode OAffinSpace is non trivial OAffinSpace-like AffinStruct ;
end;

theorem :: ANALOAF:25
for AS being non empty AffinStruct holds
( ( ex a, b being Element of AS st a <> b & ( for a, b, c, d, p, q, r, s being Element of AS holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of AS st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of AS ex d being Element of AS st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of AS st p <> b & b,p // p,c holds
ex d being Element of AS st
( a,p // p,d & a,b // c,d ) ) ) iff AS is OAffinSpace ) by Def5, STRUCT_0:def_10;

theorem Th26: :: ANALOAF:26
for V being RealLinearSpace st ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) holds
OASpace V is OAffinSpace
proof
let V be RealLinearSpace; ::_thesis: ( ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies OASpace V is OAffinSpace )
assume A1: ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; ::_thesis: OASpace V is OAffinSpace
then A2: ( ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ) ) by Th23;
A3: for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) by A1, Th23;
 ( ex a, b being Element of (OASpace V) st a <> b & ( for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) ) by A1, Th23;
hence  OASpace V is OAffinSpace by A2, A3, Def5, STRUCT_0:def_10; ::_thesis: verum
end;

definition
let IT be OAffinSpace;
attrIT is 2-dimensional  means :Def6: :: ANALOAF:def 6
 for a, b, c, d being Element of IT st not a,b // c,d & not a,b // d,c holds
ex p being Element of IT st
( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) );
end;

:: deftheorem Def6 defines 2-dimensional ANALOAF:def_6_:_
 for IT being OAffinSpace holds
( IT is 2-dimensional iff for a, b, c, d being Element of IT st not a,b // c,d & not a,b // d,c holds
ex p being Element of IT st
( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) );

registration
cluster non empty non trivial strict OAffinSpace-like 2-dimensional for AffinStruct ;
existence
 ex b1 being OAffinSpace st
( b1 is strict & b1 is 2-dimensional )
proof
consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
reconsider S = OASpace V as OAffinSpace by A1, Th26;
 for a, b, c, d being Element of S st not a,b // c,d & not a,b // d,c holds
ex p being Element of S st
( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) by A1, Th24;
then  S is 2-dimensional by Def6;
hence  ex b1 being OAffinSpace st
( b1 is strict & b1 is 2-dimensional ) ; ::_thesis: verum
end;
end;

definition
mode OAffinPlane is 2-dimensional OAffinSpace;
end;

theorem :: ANALOAF:27
for AS being non empty AffinStruct holds
( ( ex a, b being Element of AS st a <> b & ( for a, b, c, d, p, q, r, s being Element of AS holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) & ex a, b, c, d being Element of AS st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of AS ex d being Element of AS st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of AS st p <> b & b,p // p,c holds
ex d being Element of AS st
( a,p // p,d & a,b // c,d ) ) & ( for a, b, c, d being Element of AS st not a,b // c,d & not a,b // d,c holds
ex p being Element of AS st
( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) ) ) iff AS is OAffinPlane ) by Def5, Def6, STRUCT_0:def_10;

theorem :: ANALOAF:28
for V being RealLinearSpace st ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) holds
OASpace V is OAffinPlane
proof
let V be RealLinearSpace; ::_thesis: ( ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) implies OASpace V is OAffinPlane )
set S = OASpace V;
assume A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) ; ::_thesis: OASpace V is OAffinPlane
then  for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex p being Element of (OASpace V) st
( ( a,b // a,p or a,b // p,a ) & ( c,d // c,p or c,d // p,c ) ) by Th24;
hence  OASpace V is OAffinPlane by A1, Def6, Th26; ::_thesis: verum
end;