let V be RealLinearSpace; for u, u1, v, v1 being VECTOR of V
for p, q, p1, q1 being Element of (OASpace V) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v // u1,v1 )
let u, u1, v, v1 be VECTOR of V; for p, q, p1, q1 being Element of (OASpace V) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v // u1,v1 )
A1:
OASpace V = AffinStruct(# the carrier of V,(DirPar V) #)
by ANALOAF:def 4;
let p, q, p1, q1 be Element of (OASpace V); ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff u,v // u1,v1 ) )
assume A2:
( p = u & q = v & p1 = u1 & q1 = v1 )
; ( p,q // p1,q1 iff u,v // u1,v1 )
A3:
now ( u,v // u1,v1 implies p,q // p1,q1 )assume
u,
v // u1,
v1
;
p,q // p1,q1then
[[p,q],[p1,q1]] in the
CONGR of
(OASpace V)
by A2, A1, ANALOAF:22;
hence
p,
q // p1,
q1
by ANALOAF:def 2;
verum end;
now ( p,q // p1,q1 implies u,v // u1,v1 )assume
p,
q // p1,
q1
;
u,v // u1,v1then
[[u,v],[u1,v1]] in DirPar V
by A2, A1, ANALOAF:def 2;
hence
u,
v // u1,
v1
by ANALOAF:22;
verum end;
hence
( p,q // p1,q1 iff u,v // u1,v1 )
by A3; verum