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