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)

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

hence
SemiringProduct S is Subset-Family of (product X)
; :: thesis: verum
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

end;assume A1: x in SPS ; :: thesis: x in bool (product X)

reconsider x1 = x as set by TARSKI:1;

x1 c= product X

proof

hence
x in bool (product X)
; :: thesis: verum
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;

end;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

hence
t in product X
by A12a, A5, A8, A7, CARD_3:def 5; :: thesis: verumu . 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;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