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