let V be RealLinearSpace; for u, v, w, y being VECTOR of V holds
( [[u,v],[w,y]] in DirPar V iff u,v // w,y )
let u, v, w, y be VECTOR of V; ( [[u,v],[w,y]] in DirPar V iff u,v // w,y )
thus
( [[u,v],[w,y]] in DirPar V implies u,v // w,y )
( u,v // w,y implies [[u,v],[w,y]] in DirPar V )proof
assume
[[u,v],[w,y]] in DirPar V
;
u,v // w,y
then consider u9,
v9,
w9,
y9 being
VECTOR of
V such that A1:
[u,v] = [u9,v9]
and A2:
[w,y] = [w9,y9]
and A3:
u9,
v9 // w9,
y9
by Def3;
A4:
w = w9
by A2, XTUPLE_0:1;
(
u = u9 &
v = v9 )
by A1, XTUPLE_0:1;
hence
u,
v // w,
y
by A2, A3, A4, XTUPLE_0:1;
verum
end;
thus
( u,v // w,y implies [[u,v],[w,y]] in DirPar V )
by Def3; verum