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 ;
Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by ;
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 ;
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 ;
consider v2 being VECTOR of V such that
A13: Ortm (x,y,v2) = v by ;
Ortm (x,y,u2), Ortm (x,y,v2) // u,v by ;
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 ;
consider v2 being VECTOR of V such that
A17: Ortm (x,y,v2) = v1 by ;
Ortm (x,y,u2), Ortm (x,y,v2) // u1,v1 by ;
then A18: u2,v2,u1,v1 are_COrtm_wrt x,y ;
Ortm (x,y,u2), Ortm (x,y,v2) // u,v by ;
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 ; :: 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 ;
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