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

proof

let v, u be VECTOR of (DualSp 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 V st w in W holds
w,v + u are_orthogonal

proof

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

end;

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

end;

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

proof

let a be Real; :: thesis: for v being VECTOR of (DualSp V) st v in A holds
a * v in A
let v be VECTOR of (DualSp 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 (DualSp V) st
( v = v9 & ( for w being VECTOR of V st w in W holds
w,v9 are_orthogonal ) ) ;
for w being VECTOR of V st w in W holds
w,a * v are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in W implies w,a * v are_orthogonal )
assume w in W ; :: thesis: w,a * v are_orthogonal
then A8: w,v are_orthogonal by A7;
w .|. (a * v) = a * 0 by A8, DUALSP01:30;
hence w,a * v 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 DualSp V st the carrier of b₁ = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in W holds
w,v are_orthogonal } by A6, RLSUB_1:35; :: thesis: verum