let X be set ; for n being non zero Nat holds Product (n,X) c= bool (Funcs ((Seg n),(union X)))
let n be non zero Nat; Product (n,X) c= bool (Funcs ((Seg n),(union X)))
let x be object ; TARSKI:def 3 ( not x in Product (n,X) or x in bool (Funcs ((Seg n),(union X))) )
assume
x in Product (n,X)
; 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)
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; verum