let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for p, q, u, v, v' being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v' = u + (A * (p - q)) holds
v = v'
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for p, q, u, v, v' being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v' = u + (A * (p - q)) holds
v = v' )
assume A1: Gen w,y ; :: thesis: for p, q, u, v, v' being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v' = u + (A * (p - q)) holds
v = v'
let p, q, u, v, v' be VECTOR of V; :: thesis: for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v' = u + (A * (p - q)) holds
v = v'
let A be Real; :: thesis: ( p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) & v' = u + (A * (p - q)) implies v = v' )
assume that
A2: p,q,u,v are_DTr_wrt w,y and
A3: p <> q and
A4: A = ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " ) and
A5: v' = u + (A * (p - q)) ; :: thesis: v = v'
set s = p # q;
A6: PProJ w,y,(p - q),(p - q) <> 0 by A1, A3, Th37;
A7: ( p,q // u,v' or p,q // v',u )

proof

1 * (v' - u) = (u + (A * (p - q))) - u by A5, RLVECT_1:def 9
.= A * (p - q) by RLSUB_2:78 ;
then ( q,p // u,v' or q,p // v',u ) by ANALMETR:18;
hence ( p,q // u,v' or p,q // v',u ) by ANALOAF:21; :: thesis: verum

end;

( p,q,p # q,u # v' are_Ort_wrt w,y & u,v',p # q,u # v' are_Ort_wrt w,y & p,q,p # q,v' # u are_Ort_wrt w,y & v',u,p # q,v' # u are_Ort_wrt w,y )

proof

set X = PProJ w,y,(p - q),((v' # u) - (p # q));
A8: 2 * (PProJ w,y,(p - q),((v' # u) - (p # q))) = 2 * ((PProJ w,y,(p - q),(v' # u)) - (PProJ w,y,(p - q),(p # q))) by A1, Th32
.= (2 * (PProJ w,y,(p - q),(v' # u))) - (2 * (PProJ w,y,(p - q),(p # q)))
.= ((PProJ w,y,(p - q),v') + (PProJ w,y,(p - q),u)) - (2 * (PProJ w,y,(p - q),(p # q))) by A1, Th36
.= ((PProJ w,y,(p - q),v') + (PProJ w,y,(p - q),u)) - ((PProJ w,y,(p - q),p) + (PProJ w,y,(p - q),q)) by A1, Th36
.= ((PProJ w,y,(p - q),(u + (A * (p - q)))) + (PProJ w,y,(p - q),u)) - (PProJ w,y,(p - q),(p + q)) by A1, A5, Th32
.= (((PProJ w,y,(p - q),u) + (PProJ w,y,(p - q),(A * (p - q)))) + (PProJ w,y,(p - q),u)) - (PProJ w,y,(p - q),(p + q)) by A1, Th32 ;
PProJ w,y,(p - q),(A * (p - q)) = (((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " )) * (PProJ w,y,(p - q),(p - q)) by A1, A4, Th33
.= ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * (((PProJ w,y,(p - q),(p - q)) " ) * (PProJ w,y,(p - q),(p - q)))
.= ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * 1 by A6, XCMPLX_0:def 7
.= (PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u)) ;
then q,p,p # q,v' # u are_Ort_wrt w,y by A1, A8, Th35;
then p # q,v' # u,q,p are_Ort_wrt w,y by A1, Lm4A;
then A9: p # q,v' # u,p,q are_Ort_wrt w,y by A1, Lm4;
set Y = PProJ w,y,(v' - u),((v' # u) - (p # q));
A10: 2 * (PProJ w,y,(v' - u),((v' # u) - (p # q))) = 2 * ((PProJ w,y,(v' - u),(v' # u)) - (PProJ w,y,(v' - u),(p # q))) by A1, Th32
.= (2 * (PProJ w,y,(v' - u),(v' # u))) - (2 * (PProJ w,y,(v' - u),(p # q)))
.= ((PProJ w,y,(v' - u),v') + (PProJ w,y,(v' - u),u)) - (2 * (PProJ w,y,(v' - u),(p # q))) by A1, Th36
.= ((PProJ w,y,(v' - u),v') + (PProJ w,y,(v' - u),u)) - ((PProJ w,y,(v' - u),p) + (PProJ w,y,(v' - u),q)) by A1, Th36
.= ((PProJ w,y,(v' - u),(u + (A * (p - q)))) + (PProJ w,y,(v' - u),u)) - (PProJ w,y,(v' - u),(p + q)) by A1, A5, Th32
.= (((PProJ w,y,(v' - u),u) + (PProJ w,y,(v' - u),(A * (p - q)))) + (PProJ w,y,(v' - u),u)) - (PProJ w,y,(v' - u),(p + q)) by A1, Th32 ;
A11: v' - u = A * (p - q) by A5, RLSUB_2:78;
PProJ w,y,(A * (p - q)),(A * (p - q)) = A * (PProJ w,y,(p - q),(A * (p - q))) by A1, Th33
.= A * ((((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * ((PProJ w,y,(p - q),(p - q)) " )) * (PProJ w,y,(p - q),(p - q))) by A1, A4, Th33
.= A * (((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * (((PProJ w,y,(p - q),(p - q)) " ) * (PProJ w,y,(p - q),(p - q))))
.= A * (((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) * 1) by A6, XCMPLX_0:def 7
.= A * ((PProJ w,y,(p - q),(p + q)) - (2 * (PProJ w,y,(p - q),u))) ;
then A12: 2 * (PProJ w,y,(v' - u),((v' # u) - (p # q))) = (((PProJ w,y,(A * (p - q)),u) + ((A * (PProJ w,y,(p - q),(p + q))) - (A * (2 * (PProJ w,y,(p - q),u))))) + (PProJ w,y,(A * (p - q)),u)) - (PProJ w,y,(A * (p - q)),(p + q)) by A10, A11
.= (((PProJ w,y,(A * (p - q)),u) + ((PProJ w,y,(A * (p - q)),(p + q)) - (2 * (A * (PProJ w,y,(p - q),u))))) + (PProJ w,y,(A * (p - q)),u)) - (PProJ w,y,(A * (p - q)),(p + q)) by A1, Th33
.= (((PProJ w,y,(A * (p - q)),u) + ((PProJ w,y,(A * (p - q)),(p + q)) - (2 * (PProJ w,y,(A * (p - q)),u)))) + (PProJ w,y,(A * (p - q)),u)) - (PProJ w,y,(A * (p - q)),(p + q)) by A1, Th33
.= 0 ;
then u,v',p # q,v' # u are_Ort_wrt w,y by A1, Th35;
then p # q,v' # u,u,v' are_Ort_wrt w,y by A1, Lm4A;
then p # q,v' # u,v',u are_Ort_wrt w,y by A1, Lm4;
hence ( p,q,p # q,u # v' are_Ort_wrt w,y & u,v',p # q,u # v' are_Ort_wrt w,y & p,q,p # q,v' # u are_Ort_wrt w,y & v',u,p # q,v' # u are_Ort_wrt w,y ) by A1, A9, A12, Lm4A, Th35; :: thesis: verum

end;

then ( p,q,u,v' are_DTr_wrt w,y or p,q,v',u are_DTr_wrt w,y ) by A7, Def3;
hence v = v' by A1, A2, A3, Th27; :: thesis: verum