let n be Nat; :: thesis: for D being non empty set
for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1
let D be non empty set ; :: thesis: for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1
let D1 be non empty Subset of D; :: thesis: (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1
n -tuples_on D1 c= n -tuples_on D
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in n -tuples_on D1 or z in n -tuples_on D )
assume z in n -tuples_on D1 ; :: thesis: z in n -tuples_on D
then z is Tuple of n,D1 by FINSEQ_2:131;
then z is Element of n -tuples_on D by FINSEQ_2:109;
hence z in n -tuples_on D ; :: thesis: verum
end;
hence (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 by XBOOLE_1:28; :: thesis: verum