let n be Nat; :: thesis: for X being set
for S being Subset-Family of X holds Product (n,S) is Subset-Family of (product ((Seg n) --> X))
let X be set ; :: thesis: for S being Subset-Family of X holds Product (n,S) is Subset-Family of (product ((Seg n) --> X))
let S be Subset-Family of X; :: thesis: Product (n,S) is Subset-Family of (product ((Seg n) --> X))
reconsider SPS = Product (n,S) as Subset of (bool (Funcs ((dom ((Seg n) --> S)),(union (Union ((Seg n) --> S)))))) by Th36;
SPS c= bool (product ((Seg n) --> X))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SPS or x in bool (product ((Seg n) --> X)) )
assume A1: x in SPS ; :: thesis: x in bool (product ((Seg n) --> X))
reconsider x1 = x as set by TARSKI:1;
x1 c= product ((Seg n) --> X)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x1 or t in product ((Seg n) --> X) )
assume A2: t in x1 ; :: thesis: t in product ((Seg n) --> X)
consider g being Function such that
A3: x1 = product g and
A4: g in product ((Seg n) --> S) by A1, Def2;
A5: dom g = dom ((Seg n) --> 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 ((Seg n) --> S) and
A12: for y being object st y in dom ((Seg n) --> S) holds
w . y in ((Seg n) --> S) . y by A4, CARD_3:def 5;
A13: ( dom ((Seg n) --> S) = Seg n & dom ((Seg n) --> X) = Seg n ) by FUNCOP_1:13;

now :: thesis: for a being object st a in dom ((Seg n) --> X) holds
u . a in ((Seg n) --> X) . a

let a be object ; :: thesis: ( a in dom ((Seg n) --> X) implies u . a in ((Seg n) --> X) . a )
assume A14: a in dom ((Seg n) --> X) ; :: thesis: u . a in ((Seg n) --> X) . a
then reconsider a1 = a as Nat ;
( u . a in g . a & g . a in ((Seg n) --> S) . a ) by A14, A13, A10, A12, A9, A5;
then A15: ( u . a in union (((Seg n) --> S) . a) & a in Seg n ) by A14, TARSKI:def 4;
union (((Seg n) --> S) . a) c= ((Seg n) --> X) . a

proof

A16: ( ((Seg n) --> S) . a = S & ((Seg n) --> X) . a = X ) by A14, FUNCOP_1:7;
union S c= union (bool X) by ZFMISC_1:77;
hence union (((Seg n) --> S) . a) c= ((Seg n) --> X) . a by A16, ZFMISC_1:81; :: thesis: verum

end;

hence u . a in ((Seg n) --> X) . a by A15; :: thesis: verum

end;

hence t in product ((Seg n) --> X) by A13, A5, A8, A7, CARD_3:def 5; :: thesis: verum

end;

hence x in bool (product ((Seg n) --> X)) ; :: thesis: verum

end;

hence Product (n,S) is Subset-Family of (product ((Seg n) --> X)) ; :: thesis: verum