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
( Y is OrthogonalFamily of X & ( for x being Point of X st x in Y holds
x .|. x = 1 ) ) by BHSP_5:def 9;
then A2: Z is OrthogonalFamily of X by A1, Th4;
for x being Point of X st x in Z holds
x .|. x = 1 by A1, BHSP_5:def 9;
hence Z is OrthonormalFamily of X by A2, BHSP_5:def 9; :: thesis: verum