let X be RealUnitarySpace; :: thesis: for Y being OrthonormalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthonormalFamily of X
let Y be OrthonormalFamily of X; :: thesis: for Z being Subset of X st Z is Subset of Y holds
Z is OrthonormalFamily of X
let Z be Subset of X; :: thesis: ( Z is Subset of Y implies Z is OrthonormalFamily of X )
assume A1: Z is Subset of Y ; :: thesis: Z is OrthonormalFamily of X
then A2: for x being Point of X 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