let V be RealLinearSpace; :: thesis: for u, v, u1, 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, v, u1, v1 be VECTOR of V; :: thesis: 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 p, q, p1, q1 be Element of (OASpace V); :: thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff u,v // u1,v1 ) )
assume A1:
( p = u & q = v & p1 = u1 & q1 = v1 )
; :: thesis: ( p,q // p1,q1 iff u,v // u1,v1 )
A2:
OASpace V = AffinStruct(# the carrier of V,(DirPar V) #)
by ANALOAF:def 4;
A3:
now assume
p,
q // p1,
q1
;
:: thesis: u,v // u1,v1then
[[u,v],[u1,v1]] in DirPar V
by A1, A2, ANALOAF:def 2;
hence
u,
v // u1,
v1
by ANALOAF:33;
:: thesis: verum end;
now assume
u,
v // u1,
v1
;
:: thesis: p,q // p1,q1then
[[p,q],[p1,q1]] in the
CONGR of
(OASpace V)
by A1, A2, ANALOAF:33;
hence
p,
q // p1,
q1
by ANALOAF:def 2;
:: thesis: verum end;
hence
( p,q // p1,q1 iff u,v // u1,v1 )
by A3; :: thesis: verum