let V be RealLinearSpace; :: thesis: for w, y, v, u1, u2 being VECTOR of V st Gen w,y & v,u1,v,u2 are_DTr_wrt w,y holds
u1 = u2
let w, y, v, u1, u2 be VECTOR of V; :: thesis: ( Gen w,y & v,u1,v,u2 are_DTr_wrt w,y implies u1 = u2 )
assume that
A1: Gen w,y and
A2: v,u1,v,u2 are_DTr_wrt w,y ; :: thesis: u1 = u2
A3: v,u1,v # u1,v # u2 are_Ort_wrt w,y by A2, Def3;
A4: v,u2,v # u1,v # u2 are_Ort_wrt w,y by A2, Def3;
v,u1 // v,u1 by ANALOAF:8;
then A5: v,u1 '||' v,u1 by Def1;
set b = v # u1;
set c = v # u2;
A6: v,u1 // v,v # u1 by Th14;
then A7: v,u1 '||' v,v # u1 by Def1;
A8: v,u1 // v,u2 by A2, Def3;
v,u2 // v,v # u1

proof

per cases ( v = v # u1 or v <> v # u1 ) ;

suppose v = v # u1 ; :: thesis: v,u2 // v,v # u1

hence v,u2 // v,v # u1 by ANALOAF:9; :: thesis: verum

end;

suppose v <> v # u1 ; :: thesis: v,u2 // v,v # u1

then v <> u1 ;
hence v,u2 // v,v # u1 by A8, A6, ANALOAF:11; :: thesis: verum

end;

end;

end;

then A9: v,u2 '||' v,v # u1 by Def1;
v,u2 // v,v by ANALOAF:9;
then A10: v,u2 '||' v,v by Def1;
A11: v,u2 // v,v # u2 by Th14;
then A12: v,u2 '||' v,v # u2 by Def1;
A13: v,u2 // v,u1 by A8, ANALOAF:12;
v,u1 // v,v # u2

proof

per cases ( v = v # u2 or v <> v # u2 ) ;

suppose v = v # u2 ; :: thesis: v,u1 // v,v # u2

hence v,u1 // v,v # u2 by ANALOAF:9; :: thesis: verum

end;

suppose v <> v # u2 ; :: thesis: v,u1 // v,v # u2

then v <> u2 ;
hence v,u1 // v,v # u2 by A13, A11, ANALOAF:11; :: thesis: verum

end;

end;

end;

then A14: v,u1 '||' v,v # u2 by Def1;
v,u2 // v,u2 by ANALOAF:8;
then A15: v,u2 '||' v,u2 by Def1;
v,u1 // v,v by ANALOAF:9;
then A16: v,u1 '||' v,v by Def1;
assume A17: u1 <> u2 ; :: thesis: contradiction

per cases ( v <> u1 or v <> u2 ) by A17;

suppose A18: v <> u1 ; :: thesis: contradiction

then v,u1 '||' v # u1,v # u2 by A1, A7, A5, A16, A14, Lm11;
then v # u1,v # u2,v # u1,v # u2 are_Ort_wrt w,y by A1, A3, A18, Lm10;
hence contradiction by A1, A17, Lm8, Th9; :: thesis: verum

end;

suppose A19: v <> u2 ; :: thesis: contradiction

then v,u2 '||' v # u1,v # u2 by A1, A12, A15, A10, A9, Lm11;
then v # u1,v # u2,v # u1,v # u2 are_Ort_wrt w,y by A1, A4, A19, Lm10;
hence contradiction by A1, A17, Lm8, Th9; :: thesis: verum

end;

end;