:: Tuples, Projections and Cartesian Products
::  by Andrzej Trybulec
::
:: Received March 30, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, MCART_1,
   XTUPLE_0, RECDEF_2, FACIRC_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1,
   XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1;
 constructors TARSKI, ENUMSET1, XTUPLE_0, SUBSET_1, FUNCT_1;
 registrations XBOOLE_0, RELAT_1, XTUPLE_0, SUBSET_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, RELAT_1, XTUPLE_0;
 theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, FUNCT_1,
      RELAT_1, XTUPLE_0, XREGULAR;
 schemes FUNCT_1;

begin

reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2, X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5,
  Z,Z1,Z2,Z3,Z4,Z5 for set;

reserve p for pair set;

::
::   Ordered pairs
::
::  Now we introduce the projections of ordered pairs (functions that assign
::  to an ordered pair its first and its second element). The definitions
::  are permissive, function are defined for an arbitrary object. If it is not
::  an ordered pair, they are of course meaningless.

canceled 6;

theorem Th7:
  [x,y]`1=x & [x,y]`2=y;

theorem Th8:
  [p`1,p`2] = p;

theorem
  X <> {} implies ex v st v in X & not ex x,y st (x in X or y in X) & v
  = [x,y]
proof
  assume X <> {};
  then consider Y such that
A1: Y in X and
A2: not ex Y1 st Y1 in Y & not Y1 misses X by XREGULAR:2;
  take v = Y;
  thus v in X by A1;
  given x,y such that
A3: x in X or y in X and
A4: v = [x,y];
A5: { x,y } in Y by A4,TARSKI:def 2;
  x in { x,y } & y in { x,y } by TARSKI:def 2;
  hence contradiction by A2,A5,A3,XBOOLE_0:3;
end;

:: Now we prove theorems describing relationships between projections
:: of ordered pairs and Cartesian products of two sets.

theorem Th10:
  z in [:X,Y:] implies z`1 in X & z`2 in Y
proof
  assume z in [:X,Y:];
  then consider x,y such that
W: x in X & y in Y & z=[x,y] by ZFMISC_1:def 2;
   [x,y]`1 = x & [x,y]`2 = y;
  hence thesis by W;
end;

theorem
  (ex x,y st z=[x,y]) & z`1 in X & z`2 in Y implies z in [:X,Y:]
proof
  assume ex x,y st z=[x,y];
  then [z`1,z`2]=z by Th8;
  hence thesis by ZFMISC_1:def 2;
end;

theorem
  z in [:{x},Y:] implies z`1=x & z`2 in Y
proof
  assume
A1: z in [:{x},Y:];
  then z`1 in {x} by Th10;
  hence thesis by A1,Th10,TARSKI:def 1;
end;

theorem
  z in [:X,{y}:] implies z`1 in X & z`2 = y
proof
  assume
A1: z in [:X,{y}:];
  then z`2 in {y} by Th10;
  hence thesis by A1,Th10,TARSKI:def 1;
end;

theorem
  z in [:{x},{y}:] implies z`1 = x & z`2 = y
proof
  assume z in [:{x},{y}:];
  then z`1 in {x} & z`2 in {y} by Th10;
  hence thesis by TARSKI:def 1;
end;

theorem
  z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y
proof
  assume
A1: z in [:{x1,x2},Y:];
  then z`1 in {x1,x2} by Th10;
  hence thesis by A1,Th10,TARSKI:def 2;
end;

theorem
  z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2)
proof
  assume
A1: z in [:X,{y1,y2}:];
  then z`2 in {y1,y2} by Th10;
  hence thesis by A1,Th10,TARSKI:def 2;
end;

theorem
  z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y
proof
  assume z in [:{x1,x2},{y}:];
  then z`1 in {x1,x2} & z`2 in {y} by Th10;
  hence thesis by TARSKI:def 1,def 2;
end;

theorem
  z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2)
proof
  assume z in [:{x},{y1,y2}:];
  then z`1 in {x} & z`2 in {y1,y2} by Th10;
  hence thesis by TARSKI:def 1,def 2;
end;

theorem
  z in [:{x1,x2},{y1,y2}:] implies (z`1 = x1 or z`1 = x2) & (z`2 = y1 or
  z`2 = y2)
proof
  assume z in [:{x1,x2},{y1,y2}:];
  then z`1 in {x1,x2} & z`2 in {y1,y2} by Th10;
  hence thesis by TARSKI:def 2;
end;

theorem Th20:
  (ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2
proof
  given y,z such that
A1: x = [y,z];
X: [y,z]`1 = y & [y,z]`2 = z;
  now
    assume y = x;
    then {{y,z},{y}} in {y} by A1,TARSKI:def 1;
    hence contradiction by TARSKI:def 2;
  end;
  hence x <> x`1 by A1,X;
  now
    assume z = x;
    then {{y,z},{y}} in {y,z} by A1,TARSKI:def 2;
    hence contradiction by TARSKI:def 2;
  end;
  hence thesis by A1,X;
end;

:: Some of theorems proved above may be simplified , if we state them
:: for elements of Cartesian product rather than for arbitrary objects.

reserve R for Relation;

theorem Th21:
  x in R implies x = [x`1,x`2]
proof
  assume x in R;
  then ex x1,x2 st x=[x1,x2] by RELAT_1:def 1;
  hence thesis by Th8;
end;

theorem
  X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x
  = [x`1,x`2] by Th21;

Lm1: X1 <> {} & X2 <> {} implies for x being Element of [:X1,X2:] ex xx1 being
(Element of X1), xx2 being Element of X2 st x = [xx1,xx2]

proof
  assume
A1: X1 <> {} & X2 <> {};
  let x be Element of [:X1,X2:];
  reconsider xx2 = x`2 as Element of X2 by A1,Th10;
  reconsider xx1 = x`1 as Element of X1 by A1,Th10;
  take xx1,xx2;
  thus thesis by A1,Th21;
end;

theorem Th23:
  [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof
  thus [:{x1,x2},{y1,y2}:] = [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by
ZFMISC_1:109
    .= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by ZFMISC_1:30
    .= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by ZFMISC_1:30
    .= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5;
end;

theorem Th24:
  X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x
  <> x`1 & x <> x`2
proof
  assume
A1: X <> {} & Y <> {};
  let x be Element of [:X,Y:];
  x = [x`1,x`2] by A1,Th21;
  hence thesis by Th20;
end;

::
::   Triples
::

canceled;

theorem Th26:
  X <> {} implies ex v st v in X & not ex x,y,z st (x in X or y in
  X) & v = [x,y,z]
proof
  assume X <> {};
  then consider Y such that
A1: Y in X and
A2: not ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y & not Y1 misses X
  by XREGULAR:4;
  take v = Y;
  thus v in X by A1;
  given x,y,z such that
A3: x in X or y in X and
A4: v = [x,y,z];
  set Y1 = { x,y }, Y2 = { Y1,{x} }, Y3 = { Y2,z };
B5: x in Y1 & y in Y1 by TARSKI:def 2;
A6: Y3 in Y by A4,TARSKI:def 2;
  Y1 in Y2 & Y2 in Y3 by TARSKI:def 2;
  hence contradiction by A2,B5,A6,A3,XBOOLE_0:3;
end;

::
::   Quadruples
::

canceled 3;

theorem Th30:
  X <> {} implies ex v st v in X & not ex x1,x2,x3,x4 st (x1 in X
  or x2 in X) & v = [x1,x2,x3,x4]
proof
  assume X <> {};
  then consider Y such that
A1: Y in X and
A2: for Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5
  in Y holds Y1 misses X by XREGULAR:6;
  take v = Y;
  thus v in X by A1;
  given x1,x2,x3,x4 such that
A3: x1 in X or x2 in X and
A4: v = [x1,x2,x3,x4];
  set Y1 = { x1,x2 }, Y2 = { Y1,{x1} }, Y3 = { Y2,x3 }, Y4 = { Y3, {Y2}}, Y5 =
  { Y4,x4 };
A5: Y3 in Y4 & Y4 in Y5 by TARSKI:def 2;
A6: Y5 in Y by A4,TARSKI:def 2;
B7: x1 in Y1 & x2 in Y1 by TARSKI:def 2;
  Y1 in Y2 & Y2 in Y3 by TARSKI:def 2;
  hence contradiction by A2,B7,A5,A6,A3,XBOOLE_0:3;
end;

::
::   Cartesian products of three sets
::

theorem Th31:
  X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {}
proof
A1: X1 <> {} & X2 <> {} iff [:X1,X2:] <> {} by ZFMISC_1:90;
  [:[:X1,X2:],X3:] = [:X1,X2,X3:] by ZFMISC_1:def 3;
  hence thesis by A1,ZFMISC_1:90;
end;

reserve xx1 for Element of X1,
  xx2 for Element of X2,
  xx3 for Element of X3;

theorem Th32:
  X1<>{} & X2<>{} & X3<>{} implies ( [:X1,X2,X3:] = [:Y1,Y2,Y3:]
  implies X1=Y1 & X2=Y2 & X3=Y3)
proof
A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
  assume
A2: X1<>{} & X2<>{};
  assume
A4: X3<>{};
  assume [:X1,X2,X3:] = [:Y1,Y2,Y3:];
  then
A5: [:[:X1,X2:],X3:] = [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:def 3;
  then [:X1,X2:] = [:Y1,Y2:] by A2,A4,ZFMISC_1:110;
  hence thesis by A2,A4,A5,ZFMISC_1:110;
end;

theorem
  [:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 &
  X3=Y3
proof
  assume
A1: [:X1,X2,X3:]<>{};
  then
A2: X3<>{} by Th31;
  X1<>{} & X2<>{} by A1,Th31;
  hence thesis by A2,Th32;
end;

theorem
  [:X,X,X:] = [:Y,Y,Y:] implies X = Y
proof
  assume [:X,X,X:] = [:Y,Y,Y:];
  then X<>{} or Y<>{} implies thesis by Th32;
  hence thesis;
end;

Lm2: X1 <> {} & X2 <> {} & X3 <> {} implies
 for x being Element of [:X1,X2,X3:]
  ex xx1,xx2,xx3 st x = [xx1,xx2,xx3]

proof
  assume that
A1: X1 <> {} & X2 <> {} and
A2: X3 <> {};
  let x be Element of [:X1,X2,X3:];
  reconsider x9=x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
  consider x12 being (Element of [:X1,X2:]), xx3 such that
A3: x9 = [x12,xx3] by A1,A2,Lm1;
  consider xx1,xx2 such that
A4: x12 = [xx1,xx2] by A1,Lm1;
  take xx1,xx2,xx3;
  thus thesis by A3,A4;
end;

theorem Th35:
  [:{x1},{x2},{x3}:] = { [x1,x2,x3] }
proof
  thus [:{x1},{x2},{x3}:] = [:[:{x1},{x2}:],{x3}:] by ZFMISC_1:def 3
    .= [:{[x1,x2]},{x3}:] by ZFMISC_1:29
    .= { [x1,x2,x3] } by ZFMISC_1:29;
end;

theorem
  [:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] }
proof
  thus [:{x1,y1},{x2},{x3}:] = [:[:{x1,y1},{x2}:],{x3}:] by ZFMISC_1:def 3
    .= [:{[x1,x2],[y1,x2]},{x3}:] by ZFMISC_1:30
    .= { [x1,x2,x3],[y1,x2,x3] } by ZFMISC_1:30;
end;

theorem
  [:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] }
proof
  thus [:{x1},{x2,y2},{x3}:] = [:[:{x1},{x2,y2}:],{x3}:] by ZFMISC_1:def 3
    .= [:{[x1,x2],[x1,y2]},{x3}:] by ZFMISC_1:30
    .= { [x1,x2,x3],[x1,y2,x3] } by ZFMISC_1:30;
end;

theorem
  [:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] }
proof
  thus [:{x1},{x2},{x3,y3}:] = [:[:{x1},{x2}:],{x3,y3}:] by ZFMISC_1:def 3
    .= [:{[x1,x2]},{x3,y3}:] by ZFMISC_1:29
    .= { [x1,x2,x3],[x1,x2,y3] } by ZFMISC_1:30;
end;

theorem
  [:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,
  x3] }
proof
  thus [:{x1,y1},{x2,y2},{x3}:] = [:[:{x1,y1},{x2,y2}:],{x3}:] by
ZFMISC_1:def 3
    .= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3}:] by Th23
    .= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3}:] by ENUMSET1:5
    .= [:{[x1,x2],[x1,y2]},{x3}:] \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:97
    .= { [[x1,x2],x3],[[x1,y2],x3]} \/ [:{[y1,x2],[y1,y2]},{x3}:] by
ZFMISC_1:30
    .= { [[x1,x2],x3],[[x1,y2],x3]} \/ {[[y1,x2],x3],[[y1,y2],x3] } by
ZFMISC_1:30
    .= { [x1,x2,x3],[x1,y2,x3],[y1,x2,x3],[[y1,y2],x3] } by ENUMSET1:5
    .= { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] } by ENUMSET1:62;
end;

theorem
  [:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,
  y3] }
proof
  thus [:{x1,y1},{x2},{x3,y3}:] = [:[:{x1,y1},{x2}:],{x3,y3}:] by
ZFMISC_1:def 3
    .= [:{[x1,x2],[y1,x2]},{x3,y3}:] by ZFMISC_1:30
    .= { [[x1,x2],x3],[[x1,x2],y3],[[y1,x2],x3],[[y1,x2],y3] } by Th23
    .= { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] } by ENUMSET1:62;
end;

theorem
  [:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,
  y3] }
proof
  thus [:{x1},{x2,y2},{x3,y3}:] = [:[:{x1},{x2,y2}:],{x3,y3}:] by
ZFMISC_1:def 3
    .= [:{[x1,x2],[x1,y2]},{x3,y3}:] by ZFMISC_1:30
    .= { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3] } by Th23
    .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] } by ENUMSET1:62;
end;

theorem
  [:{x1,y1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,
  y2,y3], [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] }
proof
A1: [:{[x1,x2],[x1,y2]},{x3,y3}:] = { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3]
  ,[[x1,y2],y3]} by Th23
    .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} by ENUMSET1:62;
A2: [:{[y1,x2],[y1,y2]},{x3,y3}:] = { [[y1,x2],x3],[[y1,x2],y3],[[y1,y2],x3]
  ,[[y1,y2],y3]} by Th23
    .= { [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by ENUMSET1:62;
  thus [:{x1,y1},{x2,y2},{x3,y3}:] = [:[:{x1,y1},{x2,y2}:],{x3,y3}:] by
ZFMISC_1:def 3
    .= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3,y3}:] by Th23
    .= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3,y3}:] by ENUMSET1:5
    .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} \/ {[y1,x2,x3],[y1,y2,
  x3],[y1,x2,y3],[y1,y2,y3] } by A1,A2,ZFMISC_1:97
    .= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3], [y1,x2,x3],[y1,y2,x3],
  [y1,x2,y3],[y1,y2,y3] } by ENUMSET1:25;
end;

registration
 let X1,X2,X3 be non empty set;
 cluster -> triple for Element of [:X1,X2,X3:];
 coherence
  proof let x be Element of [:X1,X2,X3:];
   ex xx1 being Element of X1, xx2 being Element of X2,
           xx3 being Element of X3 st x = [xx1,xx2,xx3] by Lm2;
   hence thesis;
  end;
end;

definition
 canceled 4;
  let X1,X2,X3 be non empty set;
  let x be Element of [:X1,X2,X3:];
  redefine func x`1_3 -> Element of X1 means
  :Def5:
  x = [x1,x2,x3] implies it = x1;
  coherence
  proof
    consider xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
    [xx1,xx2,xx3]`1_3 = xx1;
   hence x`1_3 is Element of X1 by A6;
  end;
  compatibility
   proof let y be Element of X1;
    thus y = x`1_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x1
     proof assume
Z:     y = x`1_3;
      let x1,x2,x3 such that
W:     x = [x1,x2,x3];
       [x1,x2,x3]`1_3 = x1;
      hence y = x1 by W,Z;
     end;
    assume
Z:   for x1,x2,x3 holds x = [x1,x2,x3] implies y = x1;
    consider xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
     [xx1,xx2,xx3]`1_3 = xx1;
    hence y = x`1_3 by Z,A6;
   end;
  redefine func x`2_3 -> Element of X2 means
  :Def6:
  x = [x1,x2,x3] implies it = x2;
  coherence
  proof
    consider xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
    [xx1,xx2,xx3]`2_3 = xx2;
   hence x`2_3 is Element of X2 by A6;
  end;
  compatibility
   proof let y be Element of X2;
    thus y = x`2_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x2
     proof assume
Z:     y = x`2_3;
      let x1,x2,x3 such that
W:     x = [x1,x2,x3];
       [x1,x2,x3]`2_3 = x2;
      hence y = x2 by W,Z;
     end;
    assume
Z:   for x1,x2,x3 holds x = [x1,x2,x3] implies y = x2;
    consider xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
     [xx1,xx2,xx3]`2_3 = xx2;
    hence y = x`2_3 by Z,A6;
   end;
  redefine func x`3_3 -> Element of X3 means
  :Def7:
  x = [x1,x2,x3] implies it = x3;
  coherence
  proof
    consider xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
    [xx1,xx2,xx3]`3_3 = xx3;
   hence x`3_3 is Element of X3 by A6;
  end;
  compatibility
   proof let y be Element of X3;
    thus y = x`3_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x3
     proof assume
Z:     y = x`3_3;
      let x1,x2,x3 such that
W:     x = [x1,x2,x3];
       [x1,x2,x3]`3_3 = x3;
      hence y = x3 by W,Z;
     end;
    assume
Z:   for x1,x2,x3 holds x = [x1,x2,x3] implies y = x3;
    consider xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
     [xx1,xx2,xx3]`3_3 = xx3;
    hence y = x`3_3 by Z,A6;
   end;
end;

canceled;

theorem
 for X1,X2,X3 being non empty set
  for x being Element of [:X1,X2,
  X3:] holds x = [x`1_3,x`2_3,x`3_3];

theorem Th45:
  X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X =
  {}
proof
  assume that
A1: X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] and
A2: X <> {};
  [:X,Y,Z:]<>{} or [:Y,Z,X:]<>{} or [:Z,X,Y:]<>{} by A1,A2;
  then reconsider X,Y,Z as non empty set by Th31;
  per cases by A1;
  suppose
A4: X c= [:X,Y,Z:];
    consider v such that
A5: v in X and
A6: for x,y,z st x in X or y in X holds v <> [x,y,z] by Th26;
    reconsider v as Element of [:X,Y,Z:] by A4,A5;
    v = [v`1_3,v`2_3,v`3_3];
    hence contradiction by A6;
  end;
  suppose
    X c= [:Y,Z,X:];
    then X c= [:[:Y,Z:],X:] by ZFMISC_1:def 3;
    hence thesis by ZFMISC_1:111;
  end;
  suppose
A7: X c= [:Z,X,Y:];
    consider v such that
A8: v in X and
A9: for z,x,y st z in X or x in X holds v <> [z,x,y] by Th26;
    reconsider v as Element of [:Z,X,Y:] by A7,A8;
    v = [v`1_3,v`2_3,v`3_3];
    hence thesis by A9;
  end;
end;

canceled;

theorem Th47:
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
   holds x <> x`1_3 & x <> x`2_3 & x <> x`3_3
proof let X1,X2,X3 be non empty set;
  let x be Element of [:X1,X2,X3:];
  set Y9 = { x`1_3,x`2_3 }, Y = { Y9,{x`1_3}},
      X9 = { Y,x`3_3 }, X = { X9,{Y} };
A2: x = [x`1_3,x`2_3,x`3_3]
    .= [[x`1_3,x`2_3],x`3_3];
  then x = x`1_3 or x = x`2_3 implies X in Y9 & Y9 in Y & Y in X9 & X9 in X
    by TARSKI:def 2;
  hence x <> x`1_3 & x <> x`2_3 by XREGULAR:8;
  thus thesis by A2,Th20;
end;

theorem
  [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies X1 meets Y1 & X2 meets Y2 & X3
  meets Y3
proof
  assume
A1: [:X1,X2,X3:] meets [:Y1,Y2,Y3:];
A2: [:[:X1,X2:],X3:] = [:X1,X2,X3:] & [:[:Y1,Y2:],Y3:] = [:Y1,Y2,Y3:] by
ZFMISC_1:def 3;
  then [:X1,X2:] meets [:Y1,Y2:] by A1,ZFMISC_1:104;
  hence thesis by A2,A1,ZFMISC_1:104;
end;

::
::   Cartesian products of four sets
::

theorem Th49:
  [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
proof
  thus [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4
    .= [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3;
end;

theorem Th50:
  [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
proof
  thus [:[:X1,X2:],X3,X4:] = [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3
    .= [:X1,X2,X3,X4:] by Th49;
end;

theorem Th51:
  X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <>
  {}
proof
A1: [:[:X1,X2,X3:],X4:] = [:X1,X2,X3,X4:] by ZFMISC_1:def 4;
  X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {} by Th31;
  hence thesis by A1,ZFMISC_1:90;
end;

theorem Th52:
  X1<>{} & X2<>{} & X3<>{} & X4<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3
  ,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4
proof
A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
  assume
A2: X1<>{} & X2<>{} & X3<>{};
  assume
A3: X4<>{};
  assume [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:];
  then
A4: [:[:X1,X2,X3:],X4:] = [:[:Y1,Y2,Y3:],Y4:] by A1,ZFMISC_1:def 4;
   [:X1,X2,X3:] = [:Y1,Y2,Y3:] by A3,A4,A2,ZFMISC_1:110;
  hence thesis by A2,A3,A4,Th32,ZFMISC_1:110;
end;

theorem
  [:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1
  & X2=Y2 & X3=Y3 & X4=Y4
proof
  assume
A1: [:X1,X2,X3,X4:]<>{};
  then
A2: X3<>{} & X4<>{} by Th51;
  X1<>{} & X2<>{} by A1,Th51;
  hence thesis by A2,Th52;
end;

theorem
  [:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y
proof
  assume [:X,X,X,X:] = [:Y,Y,Y,Y:];
  then X<>{} or Y<>{} implies thesis by Th52;
  hence thesis;
end;

reserve xx4 for Element of X4;

Lm3: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies for x being Element of
[:X1,X2,X3,X4:] ex xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4]

proof
  assume that
A1: X1 <> {} & X2 <> {} & X3 <> {} and
A2: X4 <> {};
  let x be Element of [:X1,X2,X3,X4:];
  reconsider x9=x as Element of [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
  consider x123 being (Element of [:X1,X2,X3:]), xx4 such that
A3: x9 = [x123,xx4] by A2,Lm1,A1;
  consider xx1,xx2,xx3 such that
A4: x123 = [xx1,xx2,xx3] by A1,Lm2;
  take xx1,xx2,xx3,xx4;
  thus thesis by A3,A4;
end;

registration
 let X1,X2,X3,X4 be non empty set;
 cluster -> quadruple for Element of [:X1,X2,X3,X4:];
 coherence
  proof let x be Element of [:X1,X2,X3,X4:];
   ex xx1 being Element of X1, xx2 being Element of X2,
      xx3 being Element of X3, xx4 being Element of X4
     st x = [xx1,xx2,xx3,xx4] by Lm3;
   hence thesis;
  end;
end;

definition
  let X1,X2,X3,X4 be non empty set;
  let x be Element of [:X1,X2,X3,X4:];
  redefine func x`1_4 -> Element of X1 means
  :Def8:
  x = [x1,x2,x3,x4] implies it = x1;
  coherence
  proof
    consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
    [xx1,xx2,xx3,xx4]`1_4 = xx1;
   hence x`1_4 is Element of X1 by A6;
  end;
  compatibility
   proof let y be Element of X1;
    thus y = x`1_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
      implies y = x1
     proof assume
Z:     y = x`1_4;
      let x1,x2,x3,x4 such that
W:     x = [x1,x2,x3,x4];
       [x1,x2,x3,x4]`1_4 = x1;
      hence y = x1 by W,Z;
     end;
    assume
Z:   for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x1;
    consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
     [xx1,xx2,xx3,xx4]`1_4 = xx1;
    hence y = x`1_4 by Z,A6;
   end;
  redefine func x`2_4 -> Element of X2 means
  :Def9:
  x = [x1,x2,x3,x4] implies it = x2;
  coherence
  proof
   consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
    [xx1,xx2,xx3,xx4]`2_4 = xx2;
   hence x`2_4 is Element of X2 by A6;
  end;
  compatibility
   proof let y be Element of X2;
    thus y = x`2_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
     implies y = x2
     proof assume
Z:     y = x`2_4;
      let x1,x2,x3,x4 such that
W:     x = [x1,x2,x3,x4];
       [x1,x2,x3,x4]`2_4 = x2;
      hence y = x2 by W,Z;
     end;
    assume
Z:   for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x2;
   consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
     [xx1,xx2,xx3,xx4]`2_4 = xx2;
    hence y = x`2_4 by Z,A6;
   end;
  redefine func x`3_4 -> Element of X3 means
  :Def10:
  x = [x1,x2,x3,x4] implies it = x3;
  coherence
  proof
   consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
    [xx1,xx2,xx3,xx4]`3_4 = xx3;
   hence x`3_4 is Element of X3 by A6;
  end;
  compatibility
   proof let y be Element of X3;
    thus y = x`3_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
       implies y = x3
     proof assume
Z:     y = x`3_4;
      let x1,x2,x3,x4 such that
W:     x = [x1,x2,x3,x4];
       [x1,x2,x3,x4]`3_4 = x3;
      hence y = x3 by W,Z;
     end;
    assume
Z:   for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x3;
   consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
     [xx1,xx2,xx3,xx4]`3_4 = xx3;
    hence y = x`3_4 by Z,A6;
   end;
  redefine func x`4_4 -> Element of X4 means
  :Def11:
  x = [x1,x2,x3,x4] implies it = x4;
  coherence
  proof
   consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
    [xx1,xx2,xx3,xx4]`4_4 = xx4;
   hence x`4_4 is Element of X4 by A6;
  end;
  compatibility
   proof let y be Element of X4;
    thus y = x`4_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
       implies y = x4
     proof assume
Z:     y = x`4_4;
      let x1,x2,x3,x4 such that
W:     x = [x1,x2,x3,x4];
       [x1,x2,x3,x4]`4_4 = x4;
      hence y = x4 by W,Z;
     end;
    assume
Z:   for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x4;
   consider xx1 being Element of X1, xx2 being Element of X2,
             xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
     [xx1,xx2,xx3,xx4]`4_4 = xx4;
    hence y = x`4_4 by Z,A6;
   end;
end;

canceled;

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of
  [:X1,X2,X3,X4:] holds x = [x`1_4,x`2_4,x`3_4,x`4_4];

canceled;

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
  holds x <> x`1_4 & x <> x`2_4 & x <> x`3_4 & x <> x`4_4
proof let X1,X2,X3,X4 be non empty set;
  let x be Element of [:X1,X2,X3,X4:];
   reconsider Y = [:X1,X2:], X3, X4 as non empty set;
  reconsider x9=x as Element of [:Y,X3,X4:] by Th50;
  set Z9 = { x`1_4,x`2_4 }, Z = { Z9,{x`1_4}},
      Y9 = { Z,x`3_4 }, Y = { Y9,{Z} }, X9 =
  { Y,x`4_4 }, X = { X9,{Y} };
  x = [x`1_4,x`2_4,x`3_4,x`4_4]
    .= X;
  then
  x = x`1_4 or x = x`2_4
   implies X in Z9 & Z9 in Z & Z in Y9 & Y9 in Y & Y in X9 & X9 in X
     by TARSKI:def 2;
  hence x <> x`1_4 & x <> x`2_4 by XREGULAR:10;
  x`3_4 = (x qua set)`1`2
    .= x9`2_3;
  hence thesis by Th47;
end;

theorem
  X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2
  :] or X1 c= [:X4,X1,X2,X3:] implies X1 = {}
proof
  assume that
A1: X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,
  X2:] or X1 c= [:X4,X1,X2,X3:] and
A2: X1 <> {};
A3: [:X1,X2,X3,X4:]<>{} or [:X2,X3,X4,X1:]<>{} or [:X3,X4,X1,X2:]<>{} or [:
  X4,X1,X2,X3:]<>{} by A1,A2;
   reconsider X1,X2,X3,X4 as non empty set by A3,Th51;
  per cases by A1;
  suppose
A6: X1 c= [:X1,X2,X3,X4:];
    consider v such that
A7: v in X1 and
A8: for x1,x2,x3,x4 st x1 in X1 or x2 in X1 holds v <> [x1,x2,x3,x4]
    by Th30;
    reconsider v as Element of [:X1,X2,X3,X4:] by A6,A7;
    v = [v`1_4,v`2_4,v`3_4,v`4_4];
    hence contradiction by A8;
  end;
  suppose
    X1 c= [:X2,X3,X4,X1:];
    then X1 c= [:[:X2,X3:],X4,X1:] by Th50;
    hence thesis by Th45;
  end;
  suppose
    X1 c= [:X3,X4,X1,X2:];
    then X1 c= [:[:X3,X4:],X1,X2:] by Th50;
    hence thesis by Th45;
  end;
  suppose
A9: X1 c= [:X4,X1,X2,X3:];
    consider v such that
A10: v in X1 and
A11: for x1,x2,x3,x4 st x1 in X1 or x2 in X1 holds v <> [x1,x2,x3,x4]
    by Th30;
    reconsider v as Element of [:X4,X1,X2,X3:] by A9,A10;
    v = [v`1_4,v`2_4,v`3_4,v`4_4];
    hence thesis by A11;
  end;
end;

theorem
  [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies X1 meets Y1 & X2 meets
  Y2 & X3 meets Y3 & X4 meets Y4
proof
  assume
A1: [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:];
A2: [:[:[:X1,X2:],X3:],X4:] = [:X1,X2,X3,X4:] & [:[:[:Y1,Y2:],Y3:],Y4:] = [:
  Y1, Y2,Y3,Y4:] by Th49;
  then
A3: [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:104;
  then [:X1,X2:] meets [:Y1,Y2:] by ZFMISC_1:104;
  hence thesis by A2,A1,A3,ZFMISC_1:104;
end;

theorem
  [:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] }
proof
  thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th50
    .= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:29
    .= {[[x1,x2],x3,x4]} by Th35
    .= { [x1,x2,x3,x4] };
end;

:: Ordered pairs

theorem Th62:
  [:X,Y:] <> {} implies for x being Element of [:X,Y:] holds x <>
  x`1 & x <> x`2
proof
  assume [:X,Y:] <> {};
  then X <> {} & Y <> {} by ZFMISC_1:90;
  hence thesis by Th24;
end;

theorem
  x in [:X,Y:] implies x <> x`1 & x <> x`2 by Th62;

:: Triples

reserve A1 for Subset of X1,
  A2 for Subset of X2,
  A3 for Subset of X3,
  A4 for Subset of X4;

reserve x for Element of [:X1,X2,X3:];

theorem
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
 for x1,x2,x3 st x = [x1,x2,x3] holds
  x`1_3 = x1 & x`2_3 = x2 & x`3_3 = x3 by Def5,Def6,Def7;

theorem
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
  st for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1
 holds y1 =x`1_3
proof let X1,X2,X3 be non empty set;
  let x be Element of [:X1,X2,X3:];
  assume that
A2: for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1;
  x = [x`1_3,x`2_3,x`3_3];
  hence thesis by A2;
end;

theorem
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
  st for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds  y2 = xx2
 holds y2 =x`2_3
proof let X1,X2,X3 be non empty set;
  let x be Element of [:X1,X2,X3:];
  assume that
A2: for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y2 = xx2;
  x = [x`1_3,x`2_3,x`3_3];
  hence thesis by A2;
end;

theorem
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
  st for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3
 holds y3 =x`3_3
proof
 let X1,X2,X3 be non empty set;
  let x be Element of [:X1,X2,X3:];
  assume that
A2: for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3;
  x = [x`1_3,x`2_3,x`3_3];
  hence thesis by A2;
end;

theorem Th68:
  z in [: X1,X2,X3 :] implies ex x1,x2,x3 st x1 in X1 & x2 in X2 &
  x3 in X3 & z = [x1,x2,x3]
proof
  assume z in [: X1,X2,X3 :];
  then z in [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
  then consider x12, x3 being set such that
A1: x12 in [:X1,X2:] and
A2: x3 in X3 and
A3: z = [x12,x3] by ZFMISC_1:def 2;
  consider x1,x2 being set such that
A4: x1 in X1 & x2 in X2 and
A5: x12 = [x1,x2] by A1,ZFMISC_1:def 2;
  z = [x1,x2,x3] by A3,A5;
  hence thesis by A2,A4;
end;

theorem Th69:
  [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3
proof
A1: [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:87;
  [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
  hence thesis by A1,ZFMISC_1:87;
end;

theorem
  (for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3
  & z = [x1,x2,x3]) implies Z = [: X1,X2,X3 :]
proof
  assume
A1: for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3
  & z = [x1,x2,x3];
  now
    let z;
    thus z in Z implies z in [:[:X1,X2:],X3:]
    proof
      assume z in Z;
      then consider x1,x2,x3 such that
A2:   x1 in X1 & x2 in X2 and
A3:   x3 in X3 & z = [x1,x2,x3] by A1;
      [x1,x2] in [:X1,X2:] by A2,ZFMISC_1:def 2;
      hence thesis by A3,ZFMISC_1:def 2;
    end;
    assume z in [:[:X1,X2:],X3:];
    then consider x12,x3 being set such that
A4: x12 in [:X1,X2:] and
A5: x3 in X3 and
A6: z = [x12,x3] by ZFMISC_1:def 2;
    consider x1,x2 being set such that
A7: x1 in X1 & x2 in X2 and
A8: x12 = [x1,x2] by A4,ZFMISC_1:def 2;
    z = [x1,x2,x3] by A6,A8;
    hence z in Z by A1,A5,A7;
  end;
  then Z = [:[:X1,X2:],X3:] by TARSKI:1;
  hence thesis by ZFMISC_1:def 3;
end;

canceled;

theorem
 for X1,X2,X3 being non empty set
 for A1 being non empty Subset of X1, A2 being non empty Subset of X2,
     A3 being non empty Subset of X3
  for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:]
   holds x`1_3 in A1 & x`2_3 in A2 & x`3_3 in A3
proof
 let X1,X2,X3 be non empty set;
 let A1 be non empty Subset of X1, A2 be non empty Subset of X2,
     A3 be non empty Subset of X3;
  let x be Element of [:X1,X2,X3:];
  assume
 x in [:A1,A2,A3:];
  then reconsider y = x as Element of [:A1,A2,A3:];
A2: y`2_3 in A2;
A3: y`3_3 in A3;
  y`1_3 in A1;
  hence thesis by A2,A3;
end;

theorem Th73:
  X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,
  Y3:]
proof
A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] & [:Y1,Y2,Y3:] = [:[:Y1,Y2:],Y3:] by
ZFMISC_1:def 3;
  assume X1 c= Y1 & X2 c= Y2;
  then
A2: [:X1,X2:] c= [:Y1,Y2:] by ZFMISC_1:96;
  assume X3 c= Y3;
  hence thesis by A2,A1,ZFMISC_1:96;
end;

:: Quadruples

reserve x for Element of [:X1,X2,X3,X4:];

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 for x1,x2,x3,x4 being set st x = [x1,
  x2,x3,x4] holds x`1_4 = x1 & x`2_4 = x2 & x`3_4 = x3 & x`4_4 = x4
   by Def8,Def9,Def10,Def11;

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1
 holds y1 =x`1_4
proof
 let X1,X2,X3,X4 be non empty set;
 let x be Element of [:X1,X2,X3,X4:];
  assume that
A2: for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1;
  x = [x`1_4,x`2_4,x`3_4,x`4_4];
  hence thesis by A2;
end;

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,
  xx2,xx3,xx4] holds y2 = xx2
 holds y2 =x`2_4
proof
 let X1,X2,X3,X4 be non empty set;
 let x be Element of [:X1,X2,X3,X4:];
  assume that
A2: for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2;
  x = [x`1_4,x`2_4,x`3_4,x`4_4];
  hence thesis by A2;
end;

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,
  xx2,xx3,xx4] holds y3 = xx3
 holds y3 =x`3_4
proof
 let X1,X2,X3,X4 be non empty set;
 let x be Element of [:X1,X2,X3,X4:];
  assume that
A2: for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3;
  x = [x`1_4,x`2_4,x`3_4,x`4_4];
  hence thesis by A2;
end;

theorem
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
  st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,
  xx2,xx3,xx4] holds y4 = xx4
 holds y4 =x`4_4
proof
 let X1,X2,X3,X4 be non empty set;
 let x be Element of [:X1,X2,X3,X4:];
  assume that
A2: for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4;
  x = [x`1_4,x`2_4,x`3_4,x`4_4];
  hence thesis by A2;
end;

theorem
  z in [: X1,X2,X3,X4 :] implies ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 &
  x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4]
proof
  assume z in [: X1,X2,X3,X4 :];
  then z in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
  then consider x123, x4 being set such that
A1: x123 in [:X1,X2,X3:] and
A2: x4 in X4 and
A3: z = [x123,x4] by ZFMISC_1:def 2;
  consider x1, x2, x3 such that
A4: x1 in X1 & x2 in X2 & x3 in X3 and
A5: x123 = [x1,x2,x3] by A1,Th68;
  z = [x1,x2,x3,x4] by A3,A5;
  hence thesis by A2,A4;
end;

theorem
  [x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3
  & x4 in X4
proof
A1: [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:87;
  [:X1,X2,X3,X4:] = [:[:X1,X2:],X3,X4:] & [x1,x2,x3,x4] = [[x1,x2],x3,x4]
  by Th50;
  hence thesis by A1,Th69;
end;

theorem
  (for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in
  X3 & x4 in X4 & z = [x1,x2,x3,x4]) implies Z = [: X1,X2,X3,X4 :]
proof
  assume
A1: for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in
  X3 & x4 in X4 & z = [x1,x2,x3,x4];
  now
    let z;
    thus z in Z implies z in [:[:X1,X2,X3:],X4:]
    proof
      assume z in Z;
      then consider x1,x2,x3,x4 such that
A2:   x1 in X1 & x2 in X2 & x3 in X3 and
A3:   x4 in X4 & z = [x1,x2,x3,x4] by A1;
      [x1,x2,x3] in [:X1,X2,X3:] by A2,Th69;
      hence thesis by A3,ZFMISC_1:def 2;
    end;
    assume z in [:[:X1,X2,X3:],X4:];
    then consider x123,x4 being set such that
A4: x123 in [:X1,X2,X3:] and
A5: x4 in X4 and
A6: z = [x123,x4] by ZFMISC_1:def 2;
    consider x1,x2,x3 such that
A7: x1 in X1 & x2 in X2 & x3 in X3 and
A8: x123 = [x1,x2,x3] by A4,Th68;
    z = [x1,x2,x3,x4] by A6,A8;
    hence z in Z by A1,A5,A7;
  end;
  then Z = [:[:X1,X2,X3:],X4:] by TARSKI:1;
  hence thesis by ZFMISC_1:def 4;
end;

canceled;

theorem
 for X1,X2,X3,X4 being non empty set,
     A1 being non empty Subset of X1, A2 being non empty Subset of X2,
     A3 being non empty Subset of X3, A4 being non empty Subset of X4
  for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:]
  holds x`1_4 in A1 & x`2_4 in A2 & x`3_4 in A3 & x`4_4 in A4
proof
 let X1,X2,X3,X4 be non empty set,
     A1 be non empty Subset of X1, A2 be non empty Subset of X2,
     A3 be non empty Subset of X3, A4 be non empty Subset of X4;
  let x be Element of [:X1,X2,X3,X4:];
  assume
 x in [:A1,A2,A3,A4:];
  then reconsider y = x as Element of [:A1,A2,A3,A4:];
A2: y`2_4 in A2;
A3: y`4_4 in A4;
A4: y`3_4 in A3;
  y`1_4 in A1;
  hence thesis by A2,A4,A3;
end;

theorem Th84:
  X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4
   implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]
proof
A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] & [:Y1,Y2,Y3,Y4:] = [:[:Y1,Y2,Y3:]
  ,Y4 :] by ZFMISC_1:def 4;
  assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3;
  then
A2: [:X1,X2,X3:] c= [:Y1,Y2,Y3:] by Th73;
  assume X4 c= Y4;
  hence thesis by A2,A1,ZFMISC_1:96;
end;

definition
  let X1,X2,A1,A2;
  redefine func [:A1,A2:] -> Subset of [:X1,X2:];
  coherence by ZFMISC_1:96;
end;

definition
  let X1,X2,X3,A1,A2,A3;
  redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:];
  coherence by Th73;
end;

definition
  let X1,X2,X3,X4,A1,A2,A3,A4;
  redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:];
  coherence by Th84;
end;

begin :: Addenda

:: from DTCONSTR

definition
  let f be Function;
  func pr1 f -> Function means
  dom it = dom f & for x being set st x in dom f
  holds it.x = (f.x)`1;
  existence
  proof
    deffunc F(set) = (f.$1)`1;
    ex g being Function st dom g = dom f & for x being set st x in dom f
    holds g.x = F(x) from FUNCT_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    let p1, p2 be Function such that
A1: dom p1 = dom f and
A2: for x being set st x in dom f holds p1.x = (f.x)`1 and
A3: dom p2 = dom f and
A4: for x being set st x in dom f holds p2.x = (f.x)`1;
    now
      let x be set;
      assume
A5:   x in dom f;
      then p1.x = (f.x)`1 by A2;
      hence p1.x = p2.x by A4,A5;
    end;
    hence thesis by A1,A3,FUNCT_1:2;
  end;
  func pr2 f -> Function means
  dom it = dom f & for x being set st x in dom f
  holds it.x = (f.x)`2;
  existence
  proof
    deffunc F(set) = (f.$1)`2;
    ex g being Function st dom g = dom f & for x being set st x in dom f
    holds g.x = F(x) from FUNCT_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    let p1, p2 be Function such that
A6: dom p1 = dom f and
A7: for x being set st x in dom f holds p1.x = (f.x)`2 and
A8: dom p2 = dom f and
A9: for x being set st x in dom f holds p2.x = (f.x)`2;
    now
      let x be set;
      assume
A10:  x in dom f;
      then p1.x = (f.x)`2 by A7;
      hence p1.x = p2.x by A9,A10;
    end;
    hence thesis by A6,A8,FUNCT_1:2;
  end;
end;

definition
  let x be set;
  func x`11 equals
  x`1`1;
  coherence;
  func x`12 equals
  x`1`2;
  coherence;
  func x`21 equals
  x`2`1;
  coherence;
  func x`22 equals
  x`2`2;
  coherence;
end;

reserve x for set;

theorem
  [[x1,x2],y]`11 = x1 & [[x1,x2],y]`12 = x2 & [x,[y1,y2]]`21 = y1 & [x,[
  y1,y2]]`22 = y2;

:: missing, 2007.04.13, A.T.

theorem
  x in R implies x`1 in dom R & x`2 in rng R
proof
  assume
A1: x in R;
  then x = [x`1,x`2] by Th21;
  hence thesis by A1,XTUPLE_0:def 12,def 13;
end;

:: 2009.08.29, A.T.

theorem Th87:
 for R being non empty Relation, x being set
  holds Im(R,x) = { I`2 where I is Element of R: I`1 = x }
 proof let R be non empty Relation, x being set;
   set X = { I`2 where I is Element of R: I`1 = x };
  thus Im(R,x) c= X
   proof let z;
    assume z in Im(R,x);
     then consider y such that
A1:   [y,z] in R and
A2:   y in {x} by RELAT_1:def 13;
A3:   y = x by A2,TARSKI:def 1;
     y = [y,z]`1 & z = [y,z]`2;
    hence z in X by A1,A3;
   end;
  let z;
  assume z in X;
   then consider I being Element of R such that
A4: z= I`2 and
A5: I`1 = x;
A6: I = [I`1,I`2] by Th21;
   x in {x} by TARSKI:def 1;
  hence z in Im(R,x) by A4,A5,A6,RELAT_1:def 13;
 end;

theorem
 x in R implies x`2 in Im(R,x`1)
proof
 assume
A1: x in R;
  then x`2 in { I`2 where I is Element of R: I`1 = x`1 };
 hence thesis by A1,Th87;
end;

theorem Th89:
 x in R & y in R & x`1 = y`1 & x`2 = y`2 implies x = y
 proof assume x in R & y in R;
   then x = [x`1,x`2] & y = [y`1,y`2] by Th21;
  hence thesis;
 end;

theorem
 for R being non empty Relation, x,y being Element of R
   st x`1 = y`1 & x`2 = y`2
 holds x = y by Th89;

:: 2010.05.120, A.T.

theorem
   proj1 proj1 {[x1,x2,x3],[y1,y2,y3]} = {x1,y1}
  proof
   thus proj1 proj1 {[x1,x2,x3],[y1,y2,y3]}
       = proj1 {[x1,x2],[y1,y2]} by RELAT_1:10
      .= {x1,y1} by RELAT_1:10;
  end;

theorem
   proj1 proj1 {[x1,x2,x3]} = {x1}
   proof
   thus proj1 proj1 {[x1,x2,x3]}
       = proj1 {[x1,x2]} by RELAT_1:9
      .= {x1} by RELAT_1:9;
   end;

scheme
  BiFuncEx{A()->set,B()->set,C()->set,P[set,set,set]}: ex f,g being Function
  st dom f = A() & dom g = A() & for x st x in A() holds P[x,f.x,g.x]
provided
A1: x in A() implies ex y,z st y in B() & z in C() & P[x,y,z]
proof
  defpred H[set,set] means for y,z st $2`1 = y & $2`2 = z holds P[$1,y,z];
A2: x in A() implies ex p being set st p in [:B(),C():] & H[x,p]
  proof
    assume x in A();
    then consider y,z such that
A3: y in B() & z in C() and
A4: P[x,y,z] by A1;
    take p=[y,z];
    thus p in [:B(),C():] by A3,ZFMISC_1:87;
    thus for y,z st p`1 = y & p`2 = z holds P[x,y,z]
    proof
      let x1,x2 be set;
      assume that
A5:   p`1 = x1 and
A6:   p`2 = x2;
      x1=y by A5,Th7;
      hence thesis by A4,A6,Th7;
    end;
  end;
  consider h being Function such that
  dom h = A() & rng h c= [:B(),C():] and
A7: for x st x in A() holds H[x,h.x] from FUNCT_1:sch 5(A2);
  deffunc g(set) = (h.$1)`2;
  deffunc f(set) = (h.$1)`1;
  consider f being Function such that
A8: dom f = A() and
A9: for x st x in A() holds f.x = f(x) from FUNCT_1:sch 3;
  consider g being Function such that
A10: dom g = A() and
A11: for x st x in A() holds g.x = g(x) from FUNCT_1:sch 3;
  take f,g;
  thus dom f = A() & dom g = A() by A8,A10;
  thus for x st x in A() holds P[x,f.x,g.x]
  proof
    let x;
    assume
A12: x in A();
    then f.x = (h.x)`1 & g.x = (h.x)`2 by A9,A11;
    hence thesis by A7,A12;
  end;
end;