defpred S₁[ VECTOR of V] means for w being VECTOR of (DualSp V) st w in W holds
$1,w are_orthogonal ;
reconsider A = { v where v is VECTOR of V : S₁[v] } as Subset of V from DOMAIN_1:sch 7();
A1: for v, u being VECTOR of V st v in A & u in A holds
v + u in A

proof

let v, u be VECTOR of V; :: thesis: ( v in A & u in A implies v + u in A )
assume that
A2: v in A and
A3: u in A ; :: thesis: v + u in A
for w being VECTOR of (DualSp V) st w in W holds
v + u,w are_orthogonal

proof

let w be VECTOR of (DualSp V); :: thesis: ( w in W implies v + u,w are_orthogonal )
assume A4: w in W ; :: thesis: v + u,w are_orthogonal
ex u9 being VECTOR of V st
( u = u9 & ( for w being VECTOR of (DualSp V) st w in W holds
u9,w are_orthogonal ) ) by A3;
then A5P: u,w are_orthogonal by A4;
ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of (DualSp V) st w in W holds
v9,w are_orthogonal ) ) by A2;
then v,w are_orthogonal by A4;
then (v + u) .|. w = 0 + 0 by A5P, Th5;
hence v + u,w are_orthogonal ; :: thesis: verum

end;

hence v + u in A ; :: thesis: verum

end;

for w being VECTOR of (DualSp V) st w in W holds
0. V,w are_orthogonal by Th15;
then A6: 0. V in A ;
for a being Real
for v being VECTOR of V st v in A holds
a * v in A

proof

let a be Real; :: thesis: for v being VECTOR of V st v in A holds
a * v in A
let v be VECTOR of V; :: thesis: ( v in A implies a * v in A )
assume v in A ; :: thesis: a * v in A
then A7: ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of (DualSp V) st w in W holds
v9,w are_orthogonal ) ) ;
for w being VECTOR of (DualSp V) st w in W holds
a * v,w are_orthogonal

proof

let w be VECTOR of (DualSp V); :: thesis: ( w in W implies a * v,w are_orthogonal )
assume w in W ; :: thesis: a * v,w are_orthogonal
then A8: v,w are_orthogonal by A7;
(a * v) .|. w = a * 0 by A8, Th6;
hence a * v,w are_orthogonal ; :: thesis: verum

end;

hence a * v in A ; :: thesis: verum

end;

then A is linearly-closed by A1;
hence ex b₁ being strict Subspace of V st the carrier of b₁ = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in W holds
v,w are_orthogonal } by A6, RLSUB_1:35; :: thesis: verum