let X be RealUnitarySpace; :: thesis: for Y being OrthonormalFamily of X
for Z being Subset of st Z is Subset of holds
Z is OrthonormalFamily of X
let Y be OrthonormalFamily of X; :: thesis: for Z being Subset of st Z is Subset of holds
Z is OrthonormalFamily of X
let Z be Subset of ; :: thesis: ( Z is Subset of implies Z is OrthonormalFamily of X )
assume A1: Z is Subset of ; :: thesis: Z is OrthonormalFamily of X
then A2: for x being Point of st x in Z holds
x .|. x = 1 by BHSP_5:def 9;
Y is OrthogonalFamily of X by BHSP_5:def 9;
then Z is OrthogonalFamily of X by A1, Th4;
hence Z is OrthonormalFamily of X by A2, BHSP_5:def 9; :: thesis: verum