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