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
consider u being VECTOR of V;
thus Ortm (x,y,(0. V)) = Ortm (x,y,(0 * u)) by RLVECT_1:23
.= 0 * (Ortm (x,y,u)) by A1, Th2
.= 0. V by RLVECT_1:23 ; :: thesis: verum