let n be non zero Nat; :: thesis: for X being n -element FinSequence holds SemiringProduct X c= bool (Funcs ((dom X),(union (Union X))))
let X be n -element FinSequence; :: thesis: SemiringProduct X c= bool (Funcs ((dom X),(union (Union X))))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SemiringProduct X or x in bool (Funcs ((dom X),(union (Union X)))) )
assume x in SemiringProduct X ; :: thesis: x in bool (Funcs ((dom X),(union (Union X))))
then consider g being Function such that
A1: x = product g and
A2: g in product X by Def3;
A3: dom g = dom X by A2, CARD_3:9;
rng g c= Union X

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in Union X )
assume t in rng g ; :: thesis: t in Union X
then consider u being object such that
A4: u in dom g and
A5: t = g . u by FUNCT_1:def 3;
consider h being Function such that
A6: g = h and
A7: dom h = dom X and
A8: for v being object st v in dom X holds
h . v in X . v by A2, CARD_3:def 5;
( t in X . u & X . u in rng X ) by A6, A7, A8, A4, A5, FUNCT_1:def 3;
hence t in Union X by TARSKI:def 4; :: thesis: verum

end;

then Union g c= union (Union X) by ZFMISC_1:77;
then Funcs ((dom g),(Union g)) c= Funcs ((dom X),(union (Union X))) by A3, FUNCT_5:56;
then A9: bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((dom X),(union (Union X)))) by ZFMISC_1:67;
product g c= Funcs ((dom g),(Union g)) by FUNCT_6:1;
hence x in bool (Funcs ((dom X),(union (Union X)))) by A1, A9; :: thesis: verum