let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of holds
( [[u,v],[w,y]] in DirPar V iff u,v // w,y )
let u, v, w, y be VECTOR of ; :: thesis: ( [[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 ) :: thesis: ( u,v // w,y implies [[u,v],[w,y]] in DirPar V )

proof

assume [[u,v],[w,y]] in DirPar V ; :: thesis: u,v // w,y
then consider u', v', w', y' being VECTOR of such that
A1: [u,v] = [u',v'] and
A2: [w,y] = [w',y'] and
A3: u',v' // w',y' by Def3;
A4: w = w' by A2, ZFMISC_1:33;
( u = u' & v = v' ) by A1, ZFMISC_1:33;
hence u,v // w,y by A2, A3, A4, ZFMISC_1:33; :: thesis: verum

end;

thus ( u,v // w,y implies [[u,v],[w,y]] in DirPar V ) by Def3; :: thesis: verum