let A, B be set ; :: thesis: (A /\ B) * = (A *) /\ (B *)
set X = A /\ B;
reconsider XA = A /\ B as Subset of A ;
reconsider XB = A /\ B as Subset of B ;
( XA * c= A * & XB * c= B * ) ;
then A1: (A /\ B) * c= (A *) /\ (B *) by XBOOLE_1:19;

now :: thesis: for x being object st x in (A *) /\ (B *) holds
x in (A /\ B) *

let x be object ; :: thesis: ( x in (A *) /\ (B *) implies x in (A /\ B) * )
assume A2: x in (A *) /\ (B *) ; :: thesis: x in (A /\ B) *
reconsider pa = x as A -valued FinSequence by A2;
set m = len pa;
set mA = (len pa) -tuples_on A;
set mB = (len pa) -tuples_on B;
set mX = (len pa) -tuples_on (A /\ B);
((len pa) -tuples_on (A /\ B)) \ ((A /\ B) *) = {} ;
then A3: (len pa) -tuples_on (A /\ B) c= (A /\ B) * by XBOOLE_1:37;
reconsider pb = x as B -valued FinSequence by A2;
( pa is len pa -element & pb is len pa -element ) by CARD_1:def 7;
then ( pa in (len pa) -tuples_on A & pb in (len pa) -tuples_on B ) by Th16;
then pa in ((len pa) -tuples_on A) /\ ((len pa) -tuples_on B) by XBOOLE_0:def 4;
then pa in (len pa) -tuples_on (A /\ B) by Th3;
hence x in (A /\ B) * by A3; :: thesis: verum

end;

then (A *) /\ (B *) c= (A /\ B) * ;
hence (A /\ B) * = (A *) /\ (B *) by A1; :: thesis: verum