let X be non-empty 1 -element FinSequence; :: thesis: for S being FieldFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is Field_Subset of { <*x*> where x is Element of X . 1 : verum }
let S be FieldFamily of X; :: thesis: { (product <*s*>) where s is Element of S . 1 : verum } is Field_Subset of { <*x*> where x is Element of X . 1 : verum }
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;
dom X = Seg 1 by FINSEQ_1:89;
then A1: len X = 1 by FINSEQ_1:def 3;
A2: 1 in Seg 1 ;
then 1 in dom X by FINSEQ_1:89;
then A4: { <*x*> where x is Element of X . 1 : verum } = product <*(X . 1)*> by SRINGS_4:24;
A5: X = <*(X . 1)*> by A1, FINSEQ_1:40;
reconsider F = S . 1 as Field_Subset of (X . 1) by A2, Def3;
not F is empty ;
then consider s being object such that
A7: s in F ;
reconsider s = s as Element of S . 1 by A7;
{ (product <*s*>) where s is Element of S . 1 : verum } = SemiringProduct S by SRINGS_4:25;
then reconsider S1 = { (product <*s*>) where s is Element of S . 1 : verum } as Subset-Family of (product X) by SRINGS_4:22;

now :: thesis: for A being set st A in S1 holds
(product X) \ A in S1

let A be set ; :: thesis: ( A in S1 implies (product X) \ A in S1 )
assume A in S1 ; :: thesis: (product X) \ A in S1
then consider s being Element of S . 1 such that
A8: A = product <*s*> ;
(X . 1) \ s in F by MEASURE1:def 1;
then product <*((X . 1) \ s)*> in S1 ;
hence (product X) \ A in S1 by A5, A8, SRINGS_4:27; :: thesis: verum

end;

hence { (product <*s*>) where s is Element of S . 1 : verum } is Field_Subset of { <*x*> where x is Element of X . 1 : verum } by A4, A5, Th12, MEASURE1:def 1; :: thesis: verum