let V be RealLinearSpace; :: thesis: for u, u1, v, v1, x, y being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
let u, u1, v, v1, x, y be VECTOR of V; :: thesis: ( Gen x,y implies ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) ) )
assume A1: Gen x,y ; :: thesis: ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )
A2: ( u,v // u1,v1 implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )

proof

assume A3: u,v // u1,v1 ; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )

A4: now :: thesis: ( u = v & u1 = v1 implies ex u2 being M3( the carrier of V) ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )

assume that
A5: u = v and
A6: u1 = v1 ; :: thesis: ex u2 being M3( the carrier of V) ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
take u2 = 0. V; :: thesis: ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
take v2 = x; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
A7: Orte (x,y,u2), Orte (x,y,v2) // u,v by A5, ANALOAF:9;
Orte (x,y,u2), Orte (x,y,v2) // u1,v1 by A6, ANALOAF:9;
then A8: u2,v2,u1,v1 are_COrte_wrt x,y ;
A9: u2,v2,u,v are_COrte_wrt x,y by A7;
u2 <> v2 by A1, Lm4;
hence ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A8, A9; :: thesis: verum

end;

A10: now :: thesis: ( u <> v implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )

assume A11: u <> v ; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A12: Orte (x,y,u2) = u by A1, Th15;
consider v2 being VECTOR of V such that
A13: Orte (x,y,v2) = v by A1, Th15;
Orte (x,y,u2), Orte (x,y,v2) // u,v by A12, A13, ANALOAF:8;
then A14: u2,v2,u,v are_COrte_wrt x,y ;
u2,v2,u1,v1 are_COrte_wrt x,y by A3, A12, A13;
hence ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A11, A12, A13, A14; :: thesis: verum

end;

now :: thesis: ( u1 <> v1 implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) )

assume A15: u1 <> v1 ; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A16: Orte (x,y,u2) = u1 by A1, Th15;
consider v2 being VECTOR of V such that
A17: Orte (x,y,v2) = v1 by A1, Th15;
Orte (x,y,u2), Orte (x,y,v2) // u1,v1 by A16, A17, ANALOAF:8;
then A18: u2,v2,u1,v1 are_COrte_wrt x,y ;
Orte (x,y,u2), Orte (x,y,v2) // u,v by A3, A16, A17, ANALOAF:12;
then u2,v2,u,v are_COrte_wrt x,y ;
hence ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A15, A16, A17, A18; :: thesis: verum

end;

hence ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) by A4, A10; :: thesis: verum

end;

( ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) implies u,v // u1,v1 ) by A1, Th13, ANALOAF:11;
hence ( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y ) ) by A2; :: thesis: verum