let n be Nat; :: thesis: for S being Subset-Family of REAL holds Product (n,S) is Subset-Family of (REAL n)
let S be Subset-Family of REAL; :: thesis: Product (n,S) is Subset-Family of (REAL n)
Product (n,S) is Subset-Family of (product ((Seg n) --> REAL)) by Th37;
hence Product (n,S) is Subset-Family of (REAL n) by Th7; :: thesis: verum