let n be non zero Nat; :: thesis: ( Prod_Field (L-Field n) is SigmaField of (CarProduct ((Seg n) --> REAL)) & Prod_Measure (L-Meas n) is sigma_Measure of (Prod_Field (L-Field n)) & XProd_Field (L-Field n) is SigmaField of (product ((Seg n) --> REAL)) & XProd_Field (L-Field n) is SigmaField of (REAL n) & XProd_Measure (L-Meas n) is sigma_Measure of (XProd_Field (L-Field n)) )
product ((Seg n) --> REAL) = REAL n by SRINGS_5:8;
hence ( Prod_Field (L-Field n) is SigmaField of (CarProduct ((Seg n) --> REAL)) & Prod_Measure (L-Meas n) is sigma_Measure of (Prod_Field (L-Field n)) & XProd_Field (L-Field n) is SigmaField of (product ((Seg n) --> REAL)) & XProd_Field (L-Field n) is SigmaField of (REAL n) & XProd_Measure (L-Meas n) is sigma_Measure of (XProd_Field (L-Field n)) ) ; :: thesis: verum