let X be set ; :: thesis: for n being non zero Nat holds Product (n,X) c= bool (Funcs ((Seg n),(union X)))
let n be non zero Nat; :: thesis: Product (n,X) c= bool (Funcs ((Seg n),(union X)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Product (n,X) or x in bool (Funcs ((Seg n),(union X))) )
assume x in Product (n,X) ; :: thesis: x in bool (Funcs ((Seg n),(union X)))
then consider g being Function such that
A1: x = product g and
A2: g in product ((Seg n) --> X) by Def2;
A3: dom g = dom ((Seg n) --> X) by A2, CARD_3:9;
rng g c= Union ((Seg n) --> X)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in Union ((Seg n) --> X) )
assume t in rng g ; :: thesis: t in Union ((Seg n) --> 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 ((Seg n) --> X) and
A8: for v being object st v in dom ((Seg n) --> X) holds
h . v in ((Seg n) --> X) . v by A2, CARD_3:def 5;
( t in ((Seg n) --> X) . u & ((Seg n) --> X) . u in rng ((Seg n) --> X) ) by A6, A7, A8, A4, A5, FUNCT_1:def 3;
hence t in Union ((Seg n) --> X) by TARSKI:def 4; :: thesis: verum
end;
then Union g c= union (Union ((Seg n) --> X)) by ZFMISC_1:77;
then Funcs ((dom g),(Union g)) c= Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X)))) by A3, FUNCT_5:56;
then bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X))))) by ZFMISC_1:67;
then bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((Seg n),(union (Union ((Seg n) --> X))))) by FUNCOP_1:13;
then A11: bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((Seg n),(union X))) by CARD_3:7;
product g c= Funcs ((dom g),(Union g)) by FUNCT_6:1;
hence x in bool (Funcs ((Seg n),(union X))) by A1, A11; :: thesis: verum