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

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