let X be non-empty 1 -element FinSequence; :: thesis: for S being FieldFamily of X holds SemiringProduct S is Field_Subset of (product X)
let S be SemialgebraFamily of X; :: thesis: ( S is FieldFamily of X implies SemiringProduct S is Field_Subset of (product X) )
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;
( { (product <*s*>) where s is Element of S . 1 : verum } = SemiringProduct S & { <*x*> where x is Element of X . 1 : verum } = product X ) by SRINGS_4:23, SRINGS_4:25;
hence ( S is FieldFamily of X implies SemiringProduct S is Field_Subset of (product X) ) by Th17; :: thesis: verum