let V be RealLinearSpace; :: thesis: 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; :: 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 )

( [[u,v],[w,y]] in DirPar V iff u,v // w,y )

let u, v, w, y be VECTOR of V; :: 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

thus
( u,v // w,y implies [[u,v],[w,y]] in DirPar V )
by Def3; :: thesis: verum
assume
[[u,v],[w,y]] in DirPar V
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum