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