defpred S₁[ VECTOR of V] means for w being VECTOR of V st w in M 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();
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 V st w in M holds
w,v + u are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in M implies w,v + u are_orthogonal )
assume A4: w in M ; :: thesis: w,v + u are_orthogonal
ex u9 being VECTOR of V st
( u = u9 & ( for w being VECTOR of V st w in M holds
w,u9 are_orthogonal ) ) by A3;
then w,u are_orthogonal by A4;
then A5: w .|. u = 0 by BHSP_1:def 3;
ex v9 being VECTOR of V st
( v = v9 & ( for w being VECTOR of V st w in M holds
w,v9 are_orthogonal ) ) by A2;
then w,v are_orthogonal by A4;
then w .|. v = 0 by BHSP_1:def 3;
then w .|. (v + u) = 0 + 0 by A5, BHSP_1:2;
hence w,v + u are_orthogonal by BHSP_1:def 3; :: thesis: verum

end;

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

end;

for w being VECTOR of V st w in M holds
w, 0. V are_orthogonal

proof

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

end;

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 V st w in M holds
w,v9 are_orthogonal ) ) ;
for w being VECTOR of V st w in M holds
w,a * v are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in M implies w,a * v are_orthogonal )
assume w in M ; :: thesis: w,a * v are_orthogonal
then A8: w,v are_orthogonal by A7;
w .|. (a * v) = a * (w .|. v) by BHSP_1:3
.= 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 A1, 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 M holds
w,v are_orthogonal } by A6, RUSUB_1:29; :: thesis: verum