let A, B be set ; :: thesis: for m being Nat holds m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B)
let m be Nat; :: thesis: m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B)
m -tuples_on (A /\ B) = (m -tuples_on A) /\ (B *) by Th2
.= (m -tuples_on A) /\ (m -tuples_on B) by Th1 ;
hence m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B) ; :: thesis: verum