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

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