let V be RealLinearSpace; :: thesis: ( ex p, q being VECTOR of V st p <> q implies for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
given p, q being VECTOR of V such that A1: p <> q ; :: thesis: for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
let u, v, w be VECTOR of V; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A2: now :: thesis: ( u <> w implies ex y being M3( the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
assume A3: u <> w ; :: thesis: ex y being M3( the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
take y = (v + w) - u; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A4: now :: thesis: not v = y
assume v = y ; :: thesis: contradiction
then v = v + (w - u) by RLVECT_1:def 3;
then w - u = 0. V by RLVECT_1:9;
hence contradiction by A3, RLVECT_1:21; :: thesis: verum
end;
( u,v // w,y & u,w // v,y ) by Th16;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A4; :: thesis: verum
end;
now :: thesis: ( u = w implies ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
assume A5: u = w ; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A6: now :: thesis: ( u = v implies ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
assume u = v ; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
then A7: ( u,v // w,p & u,v // w,q ) ;
A8: ( v <> p or v <> q ) by A1;
( u,w // v,p & u,w // v,q ) by A5;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A8, A7; :: thesis: verum
end;
( u,v // w,u & u,w // v,u ) by A5;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A6; :: thesis: verum
end;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A2; :: thesis: verum