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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )
A2: ( u,v // u1,v1 implies ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
take u2 = 0. V; :: thesis: ex v2, u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
take v2 = x; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
A7: Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A5, ANALOAF:9;
Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by A6, ANALOAF:9;
then A8: u2,v2,u1,v1 are_COrtm_wrt x,y ;
A9: u2,v2,u,v are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )

assume A11: u <> v ; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A12: Ortm (x,y,u2) = u by A1, Th8;
consider v2 being VECTOR of V such that
A13: Ortm (x,y,v2) = v by A1, Th8;
Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A12, A13, ANALOAF:8;
then A14: u2,v2,u,v are_COrtm_wrt x,y ;
u2,v2,u1,v1 are_COrtm_wrt x,y by A3, A12, A13;
hence ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )

assume A15: u1 <> v1 ; :: thesis: ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A16: Ortm (x,y,u2) = u1 by A1, Th8;
consider v2 being VECTOR of V such that
A17: Ortm (x,y,v2) = v1 by A1, Th8;
Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by A16, A17, ANALOAF:8;
then A18: u2,v2,u1,v1 are_COrtm_wrt x,y ;
Ortm (x,y,u2), Ortm (x,y,v2) // u,v by A3, A16, A17, ANALOAF:12;
then u2,v2,u,v are_COrtm_wrt x,y ;
hence ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_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_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) by A4, A10; :: thesis: verum

end;

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