let x, y be set ; :: thesis: (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*>

per cases ( ( not x is empty & not y is empty & not x /\ y is empty ) or ( not x is empty & not y is empty & x /\ y is empty ) or x is empty or y is empty ) ;

suppose A1: ( not x is empty & not y is empty & not x /\ y is empty ) ; :: thesis: (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*>

then A2: ( product <*x*> = { <*t*> where t is Element of x : verum } & product <*y*> = { <*t*> where t is Element of y : verum } & product <*(x /\ y)*> = { <*t*> where t is Element of x /\ y : verum } ) by Thm23;
set Px = { <*t*> where t is Element of x : verum } ;
set Py = { <*t*> where t is Element of y : verum } ;
set Pxy = { <*t*> where t is Element of x /\ y : verum } ;

now :: thesis: ( ( for u being object st u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } holds
u in { <*t*> where t is Element of x /\ y : verum } ) & ( for u being object st u in { <*t*> where t is Element of x /\ y : verum } holds
u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } ) )

hereby :: thesis: for u being object st u in { <*t*> where t is Element of x /\ y : verum } holds
u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum }

let u be object ; :: thesis: ( u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } implies u in { <*t*> where t is Element of x /\ y : verum } )
assume u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } ; :: thesis: u in { <*t*> where t is Element of x /\ y : verum }
then A3: ( u in { <*t*> where t is Element of x : verum } & u in { <*t*> where t is Element of y : verum } ) by XBOOLE_0:def 4;
then consider ux being Element of x such that
A4: u = <*ux*> ;
consider uy being Element of y such that
A5: u = <*uy*> by A3;
ux = uy by A4, A5, FINSEQ_1:76;
then ux in x /\ y by A1, XBOOLE_0:def 4;
hence u in { <*t*> where t is Element of x /\ y : verum } by A4; :: thesis: verum

end;

let u be object ; :: thesis: ( u in { <*t*> where t is Element of x /\ y : verum } implies u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } )
assume u in { <*t*> where t is Element of x /\ y : verum } ; :: thesis: u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum }
then consider uxy being Element of x /\ y such that
A6: u = <*uxy*> ;
( uxy is Element of x & uxy is Element of y ) by A1, XBOOLE_0:def 4;
then ( u in { <*t*> where t is Element of x : verum } & u in { <*t*> where t is Element of y : verum } ) by A6;
hence u in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } by XBOOLE_0:def 4; :: thesis: verum

end;

then ( { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } c= { <*t*> where t is Element of x /\ y : verum } & { <*t*> where t is Element of x /\ y : verum } c= { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } ) ;
hence (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*> by A2; :: thesis: verum

end;

suppose A7: ( not x is empty & not y is empty & x /\ y is empty ) ; :: thesis: (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*>

then A8: ( product <*x*> = { <*t*> where t is Element of x : verum } & product <*y*> = { <*t*> where t is Element of y : verum } ) by Thm23;
set Px = { <*t*> where t is Element of x : verum } ;
set Py = { <*t*> where t is Element of y : verum } ;
{ <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } c= {}

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } or t in {} )
assume t in { <*t*> where t is Element of x : verum } /\ { <*t*> where t is Element of y : verum } ; :: thesis: t in {}
then A9: ( t in { <*t*> where t is Element of x : verum } & t in { <*t*> where t is Element of y : verum } ) by XBOOLE_0:def 4;
then consider t1 being Element of x such that
A10: t = <*t1*> ;
consider t2 being Element of y such that
A11: t = <*t2*> by A9;
t1 = t2 by A10, A11, FINSEQ_1:76;
hence t in {} by A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*> by A8, A7; :: thesis: verum

end;

suppose ( x is empty or y is empty ) ; :: thesis: (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*>

hence (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*> by Thm22; :: thesis: verum

end;

end;