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 Lm23
.= (m -tuples_on A) /\ (m -tuples_on B) by Lm22 ;
hence m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B) ; :: thesis: verum