let V be RealNormSpace; :: thesis: for M being Subspace of DualSp V
for v being VECTOR of V
for m being VECTOR of (DualSp V) st v in Ort_Comp M & m in M holds
v .|. m = 0
let M be Subspace of DualSp V; :: thesis: for v being VECTOR of V
for m being VECTOR of (DualSp V) st v in Ort_Comp M & m in M holds
v .|. m = 0
let v be VECTOR of V; :: thesis: for m being VECTOR of (DualSp V) st v in Ort_Comp M & m in M holds
v .|. m = 0
let m be VECTOR of (DualSp V); :: thesis: ( v in Ort_Comp M & m in M implies v .|. m = 0 )
assume A1: ( v in Ort_Comp M & m in M ) ; :: thesis: v .|. m = 0
the carrier of (Ort_Comp M) = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in M holds
v,w are_orthogonal } by Def6;
then v in { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in M holds
v,w are_orthogonal } by A1, STRUCT_0:def 5;
then ex v0 being VECTOR of V st
( v = v0 & ( for w being VECTOR of (DualSp V) st w in M holds
v0,w are_orthogonal ) ) ;
then v,m are_orthogonal by A1;
hence v .|. m = 0 ; :: thesis: verum