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 (product X)
let X be non-empty n -element FinSequence; :: thesis: for S being SemiringFamily of X holds SemiringProduct S is Subset-Family of (product X)
let S be SemiringFamily of X; :: thesis: SemiringProduct S is Subset-Family of (product X)
reconsider SPS = SemiringProduct S as Subset of (bool (Funcs ((dom S),(union (Union S))))) by Thm19;
SPS c= bool (product X)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SPS or x in bool (product X) )
assume A1: x in SPS ; :: thesis: x in bool (product X)
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: t in product X
consider g being Function such that
A3: x1 = product g and
A4: g in product S by A1, Def3;
A5: dom g = dom S by A4, CARD_3:9;
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 A2, A3, CARD_3:def 5;
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 A4, CARD_3:def 5;
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 A13, FINSEQ_1:89;
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 A13, FINSEQ_1:89, TARSKI:def 4;
union (S . a) c= X . a by A15, Thm17;
hence u . a in X . a by A16; :: thesis: verum
end;
hence t in product X by A12a, A5, A8, A7, CARD_3:def 5; :: thesis: verum
end;
hence x in bool (product X) ; :: thesis: verum
end;
hence SemiringProduct S is Subset-Family of (product X) ; :: thesis: verum