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 } & not u in { <*t*> where t is Element of y : verum } ) by XBOOLE_0:def 5;
then consider ux being Element of x such that
A4: u = <*ux*> ;
not ux in y by A3, A4;
then ux in x \ y by A1, XBOOLE_0:def 5;
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
A5: u = <*uxy*> ;
A6: ( uxy is Element of x & uxy is not Element of y ) by A1, XBOOLE_0:def 5;
now :: thesis: not u in { <*t*> where t is Element of y : verum }
assume u in { <*t*> where t is Element of y : verum } ; :: thesis: contradiction
then consider a being Element of y such that
A7: <*uxy*> = <*a*> by A5;
thus contradiction by A7, A6, FINSEQ_1:76; :: thesis: verum
end;
then ( u in { <*t*> where t is Element of x : verum } & not u in { <*t*> where t is Element of y : verum } ) by A5, A6;
hence u in { <*t*> where t is Element of x : verum } \ { <*t*> where t is Element of y : verum } by XBOOLE_0:def 5; :: 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 A8: ( not x is empty & not y is empty & x \ y is empty ) ; :: thesis: (product <*x*>) \ (product <*y*>) = product <*(x \ y)*>
then A9: ( 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 A10: ( t in { <*t*> where t is Element of x : verum } & not t in { <*t*> where t is Element of y : verum } ) by XBOOLE_0:def 5;
then consider t1 being Element of x such that
A11: t = <*t1*> ;
not t1 in y by A10, A11;
hence t in {} by A8, XBOOLE_0:def 5; :: thesis: verum
end;
hence (product <*x*>) \ (product <*y*>) = product <*(x \ y)*> by A8, A9; :: 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;