let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds

for u, v, w being VECTOR of V ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

let x, y be VECTOR of V; :: thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )

assume A1: Gen x,y ; :: thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

let u, v, w be VECTOR of V; :: thesis: ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A2; :: thesis: verum

for u, v, w being VECTOR of V ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

let x, y be VECTOR of V; :: thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )

assume A1: Gen x,y ; :: thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

let u, v, w be VECTOR of V; :: thesis: ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

A2: now :: thesis: ( u = v implies ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )

assume A3:
u = v
; :: thesis: ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

take u1 = w + x; :: thesis: ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

Ortm (x,y,w), Ortm (x,y,u1) // u,v by A3, ANALOAF:9;

then A4: w,u1,u,v are_COrtm_wrt x,y ;

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A4; :: thesis: verum

end;( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

take u1 = w + x; :: thesis: ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

Ortm (x,y,w), Ortm (x,y,u1) // u,v by A3, ANALOAF:9;

then A4: w,u1,u,v are_COrtm_wrt x,y ;

now :: thesis: not w = u1

hence
ex u1 being VECTOR of V st assume
w = u1
; :: thesis: contradiction

then x = 0. V by RLVECT_1:9;

hence contradiction by A1, Lm4; :: thesis: verum

end;then x = 0. V by RLVECT_1:9;

hence contradiction by A1, Lm4; :: thesis: verum

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A4; :: thesis: verum

now :: thesis: ( u <> v implies ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )

hence
ex u1 being VECTOR of V st ( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) )

assume A5:
u <> v
; :: thesis: ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

consider u2 being VECTOR of V such that

A6: Ortm (x,y,u2) = u by A1, Th8;

consider v2 being VECTOR of V such that

A7: Ortm (x,y,v2) = v by A1, Th8;

take u1 = (v2 + w) - u2; :: thesis: ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

u2,v2 // w,u1 by ANALOAF:16;

then w,u1 // u2,v2 by ANALOAF:12;

then Ortm (x,y,w), Ortm (x,y,u1) // Ortm (x,y,u2), Ortm (x,y,v2) by A1, Th17;

then A8: w,u1,u,v are_COrtm_wrt x,y by A6, A7;

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A8; :: thesis: verum

end;( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

consider u2 being VECTOR of V such that

A6: Ortm (x,y,u2) = u by A1, Th8;

consider v2 being VECTOR of V such that

A7: Ortm (x,y,v2) = v by A1, Th8;

take u1 = (v2 + w) - u2; :: thesis: ex u1 being VECTOR of V st

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y )

u2,v2 // w,u1 by ANALOAF:16;

then w,u1 // u2,v2 by ANALOAF:12;

then Ortm (x,y,w), Ortm (x,y,u1) // Ortm (x,y,u2), Ortm (x,y,v2) by A1, Th17;

then A8: w,u1,u,v are_COrtm_wrt x,y by A6, A7;

now :: thesis: not w = u1

hence
ex u1 being VECTOR of V st assume
w = u1
; :: thesis: contradiction

then w = w + (v2 - u2) by RLVECT_1:def 3;

then v2 - u2 = 0. V by RLVECT_1:9;

hence contradiction by A5, A6, A7, RLVECT_1:21; :: thesis: verum

end;then w = w + (v2 - u2) by RLVECT_1:def 3;

then v2 - u2 = 0. V by RLVECT_1:9;

hence contradiction by A5, A6, A7, RLVECT_1:21; :: thesis: verum

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A8; :: thesis: verum

( w <> u1 & w,u1,u,v are_COrtm_wrt x,y ) by A2; :: thesis: verum