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,u2 & v,u1,v # u1,v # u2 are_Ort_wrt w,y & v,u2,v # u1,v # u2 are_Ort_wrt w,y ) by A2, Def3;
set b = v # u1;
set c = v # u2;
assume A4: u1 <> u2 ; :: thesis: contradiction
A5: ( v,u1 // v,u2 & v,u2 // v,u1 ) by A3, ANALOAF:21;
A6: ( v,u1 // v,v # u1 & v,u2 // v,v # u2 ) by Th14;
A7: ( v,u1 // v,u1 & v,u1 // v,v & v,u2 // v,u2 & v,u2 // v,v ) by ANALOAF:17, ANALOAF:18;
A8: v,u1 // v,v # u2

proof

now

assume v <> v # u2 ; :: thesis: v,u1 // v,v # u2
then v <> u2 ;
hence v,u1 // v,v # u2 by A5, A6, ANALOAF:20; :: thesis: verum

end;

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

end;

A9: v,u2 // v,v # u1

proof

now

assume v <> v # u1 ; :: thesis: v,u2 // v,v # u1
then v <> u1 ;
hence v,u2 // v,v # u1 by A3, A6, ANALOAF:20; :: thesis: verum

end;

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

end;

A10: ( v,u1 '||' v,v # u1 & v,u2 '||' v,v # u2 ) by A6, Def1;
A11: ( v,u1 '||' v,u1 & v,u1 '||' v,v & v,u2 '||' v,u2 & v,u2 '||' v,v ) by A7, Def1;
A12: v,u1 '||' v,v # u2 by A8, Def1;
A13: v,u2 '||' v,v # u1 by A9, Def1;

A14: now

assume A15: v <> u1 ; :: thesis: contradiction
then v,u1 '||' v # u1,v # u2 by A1, A10, A11, A12, Lm10;
then v # u1,v # u2,v # u1,v # u2 are_Ort_wrt w,y by A1, A3, A15, Lm9;
hence contradiction by A1, A4, Lm7, Th9; :: thesis: verum

end;

now

assume A16: v <> u2 ; :: thesis: contradiction
then v,u2 '||' v # u1,v # u2 by A1, A10, A11, A13, Lm10;
then v # u1,v # u2,v # u1,v # u2 are_Ort_wrt w,y by A1, A3, A16, Lm9;
hence contradiction by A1, A4, Lm7, Th9; :: thesis: verum

end;

hence contradiction by A4, A14; :: thesis: verum