let n be Nat; :: thesis: for X being set
for S being non empty Subset-Family of X holds Product (n,S) = { (product f) where f is Tuple of n,S : verum }
let X be set ; :: thesis: for S being non empty Subset-Family of X holds Product (n,S) = { (product f) where f is Tuple of n,S : verum }
let S be non empty Subset-Family of X; :: thesis: Product (n,S) = { (product f) where f is Tuple of n,S : verum }
thus Product (n,S) c= { (product f) where f is Tuple of n,S : verum } :: according to XBOOLE_0:def 10 :: thesis: { (product f) where f is Tuple of n,S : verum } c= Product (n,S)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Product (n,S) or x in { (product f) where f is Tuple of n,S : verum } )
assume x in Product (n,S) ; :: thesis: x in { (product f) where f is Tuple of n,S : verum }
then consider g being Function such that
A1: x = product g and
A2: g in product ((Seg n) --> S) by Def2;
g in n -tuples_on S by A2, Th8;
then g is Tuple of n,S by FINSEQ_2:131;
hence x in { (product f) where f is Tuple of n,S : verum } by A1; :: thesis: verum
end;
thus { (product f) where f is Tuple of n,S : verum } c= Product (n,S) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (product f) where f is Tuple of n,S : verum } or x in Product (n,S) )
assume x in { (product f) where f is Tuple of n,S : verum } ; :: thesis: x in Product (n,S)
then consider f being Tuple of n,S such that
A3: x = product f ;
f in n -tuples_on S by FINSEQ_2:131;
then f in product ((Seg n) --> S) by Th8;
hence x in Product (n,S) by A3, Def2; :: thesis: verum
end;