let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
Ortm (x,y,(0. V)) = 0. V
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies Ortm (x,y,(0. V)) = 0. V )
assume A1: Gen x,y ; :: thesis: Ortm (x,y,(0. V)) = 0. V
set u = the VECTOR of V;
thus Ortm (x,y,(0. V)) = Ortm (x,y,(0 * the VECTOR of V)) by RLVECT_1:10
.= 0 * (Ortm (x,y, the VECTOR of V)) by A1, Th2
.= 0. V by RLVECT_1:10 ; :: thesis: verum