defpred S₁[ VECTOR of 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 V : S₁[v] } as Subset of V from DOMAIN_1:sch 7();
for w being VECTOR of V st w in W holds
w, 0. V are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in W implies w, 0. V are_orthogonal )
assume w in W ; :: thesis: w, 0. V are_orthogonal
w .|. (0. V) = 0 by BHSP_1:20;
hence w, 0. V are_orthogonal by BHSP_1:def 3; :: thesis: verum

end;

then A1: 0. V in A ;
A2: 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 A3: ( v in A & 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
consider v' being VECTOR of V such that
A5: ( v = v' & ( for w being VECTOR of V st w in W holds
w,v' are_orthogonal ) ) by A3;
consider u' being VECTOR of V such that
A6: ( u = u' & ( for w being VECTOR of V st w in W holds
w,u' are_orthogonal ) ) by A3;
( w,v are_orthogonal & w,u are_orthogonal ) by A4, A5, A6;
then ( w .|. v = 0 & w .|. u = 0 ) by BHSP_1:def 3;
then w .|. (v + u) = 0 + 0 by BHSP_1:7;
hence w,v + u are_orthogonal by BHSP_1:def 3; :: thesis: verum

end;

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

end;

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 consider v' being VECTOR of V such that
A7: ( v = v' & ( for w being VECTOR of V st w in W holds
w,v' 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 * (w .|. v) by BHSP_1:8
.= a * 0 by A8, BHSP_1:def 3 ;
hence w,a * v are_orthogonal by BHSP_1:def 3; :: thesis: verum

end;

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

end;

then A is linearly-closed by A2, RLSUB_1:def 1;
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 V st w in W holds
w,v are_orthogonal } by A1, RUSUB_1:29; :: thesis: verum