let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y being VECTOR of V st Gen w,y holds
for p, q, p1, q1 being Element of the carrier of (Lambda (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, w, y be VECTOR of V; :: thesis: ( Gen w,y implies for p, q, p1, q1 being Element of the carrier of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 ) )
assume Gen w,y ; :: thesis: for p, q, p1, q1 being Element of the carrier of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 )
then reconsider S = OASpace V as OAffinSpace by Th1;
let p, q, p1, q1 be Element of the carrier of (Lambda (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 )
Lambda (OASpace V) = AffinStruct(# the carrier of (OASpace V),(lambda the CONGR of (OASpace V)) #) by DIRAF:def 2;
then reconsider p9 = p, q9 = q, p19 = p1, q19 = q1 as Element of S ;
A2: now :: thesis: ( u,v '||' u1,v1 implies p,q // p1,q1 )
assume u,v '||' u1,v1 ; :: thesis: p,q // p1,q1
then ( u,v // u1,v1 or u,v // v1,u1 ) ;
then ( p9,q9 // p19,q19 or p9,q9 // q19,p19 ) by A1, Th2;
then p9,q9 '||' p19,q19 by DIRAF:def 4;
hence p,q // p1,q1 by DIRAF:38; :: 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 p9,q9 '||' p19,q19 by DIRAF:38;
then ( p9,q9 // p19,q19 or p9,q9 // q19,p19 ) by DIRAF:def 4;
then ( u,v // u1,v1 or u,v // v1,u1 ) by A1, Th2;
hence u,v '||' u1,v1 ; :: thesis: verum
end;
hence ( p,q // p1,q1 iff u,v '||' u1,v1 ) by A2; :: thesis: verum