let V be RealLinearSpace; 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; ( 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
; 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)); ( 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 )
; ( 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 ( u,v '||' u1,v1 implies p,q // p1,q1 )assume
u,
v '||' u1,
v1
;
p,q // p1,q1then
(
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;
verum end;
now ( p,q // p1,q1 implies u,v '||' u1,v1 )assume
p,
q // p1,
q1
;
u,v '||' u1,v1then
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
;
verum end;
hence
( p,q // p1,q1 iff u,v '||' u1,v1 )
by A2; verum