let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is Subset-Family of ()

let X be non-empty n -element FinSequence; :: thesis: for S being SemiringFamily of X holds SemiringProduct S is Subset-Family of ()
let S be SemiringFamily of X; :: thesis: SemiringProduct S is Subset-Family of ()
reconsider SPS = SemiringProduct S as Subset of (bool (Funcs ((dom S),(union ())))) by Thm19;
SPS c= bool ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SPS or x in bool () )
assume A1: x in SPS ; :: thesis: x in bool ()
reconsider x1 = x as set by TARSKI:1;
x1 c= product X
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x1 or t in product X )
assume A2: t in x1 ; :: thesis:
consider g being Function such that
A3: x1 = product g and
A4: g in product S by ;
A5: dom g = dom S by ;
consider u being Function such that
A7: t = u and
A8: dom u = dom g and
A9: for v being object st v in dom g holds
u . v in g . v by ;
consider w being Function such that
A10: g = w and
dom w = dom S and
A12: for y being object st y in dom S holds
w . y in S . y by ;
A12a: dom S = dom X by Thm16;
now :: thesis: for a being object st a in dom X holds
u . a in X . a
let a be object ; :: thesis: ( a in dom X implies u . a in X . a )
assume A13: a in dom X ; :: thesis: u . a in X . a
A15: a in Seg n by ;
reconsider a1 = a as Nat by A13;
( u . a in g . a & g . a in S . a ) by A13, A12a, A10, A12, A9, A5;
then A16: ( u . a in union (S . a) & a in Seg n ) by ;
union (S . a) c= X . a by ;
hence u . a in X . a by A16; :: thesis: verum
end;
hence t in product X by ; :: thesis: verum
end;
hence x in bool () ; :: thesis: verum
end;
hence SemiringProduct S is Subset-Family of () ; :: thesis: verum