:: DOMAIN_1 semantic presentation

begin


theorem :: DOMAIN_1:1
for a being set
for X1, X2 being non empty set st a in [:X1,X2:] holds
ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]
proof
let a be set ; ::_thesis: for X1, X2 being non empty set st a in [:X1,X2:] holds
ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]
let X1, X2 be non empty set ; ::_thesis: ( a in [:X1,X2:] implies ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2] )
assume  a in [:X1,X2:] ; ::_thesis: ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]
then consider x1, x2 being set  such that
A1: x1 in X1 and
A2: x2 in X2 and
A3: a = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Element of X2 by A2;
reconsider x1 = x1 as Element of X1 by A1;
take  x1 ; ::_thesis: ex x2 being Element of X2 st a = [x1,x2]
take  x2 ; ::_thesis: a = [x1,x2]
thus  a = [x1,x2] by A3; ::_thesis: verum
end;

theorem :: DOMAIN_1:2
for X1, X2 being non empty set
for x, y being Element of [:X1,X2:] st x `1 = y `1 & x `2 = y `2 holds
x = y
proof
let X1, X2 be non empty set ; ::_thesis: for x, y being Element of [:X1,X2:] st x `1 = y `1 & x `2 = y `2 holds
x = y
let x, y be Element of [:X1,X2:]; ::_thesis: ( x `1 = y `1 & x `2 = y `2 implies x = y )
 [(x `1),(x `2)] = x by MCART_1:21;
hence  ( x `1 = y `1 & x `2 = y `2 implies x = y ) by MCART_1:21; ::_thesis: verum
end;

definition
let X1, X2 be non empty set ;
let x1 be Element of X1;
let x2 be Element of X2;
:: original: [
redefine func[x1,x2] ->  Element of [:X1,X2:];
coherence
 [x1,x2] is Element of [:X1,X2:] by ZFMISC_1:87;
end;

definition
let X1, X2 be non empty set ;
let x be Element of [:X1,X2:];
:: original: `1
redefine funcx `1  ->  Element of X1;
coherence
 x `1 is Element of X1 by MCART_1:10;
:: original: `2
redefine funcx `2  ->  Element of X2;
coherence
 x `2 is Element of X2 by MCART_1:10;
end;

theorem Th3: :: DOMAIN_1:3
for a being set
for X1, X2, X3 being non empty set holds
( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] )
proof
let a be set ; ::_thesis: for X1, X2, X3 being non empty set holds
( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] )
let X1, X2, X3 be non empty set ; ::_thesis: ( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] )
thus  ( a in [:X1,X2,X3:] implies ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ::_thesis: ( ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] implies a in [:X1,X2,X3:] )
proof
assume  a in [:X1,X2,X3:] ; ::_thesis: ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3]
then  a 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: a = [x12,x3] by ZFMISC_1:def_2;
reconsider x3 = x3 as Element of X3 by A2;
consider x1, x2 being set  such that
A4: x1 in X1 and
A5: x2 in X2 and
A6: x12 = [x1,x2] by A1, ZFMISC_1:def_2;
reconsider x2 = x2 as Element of X2 by A5;
reconsider x1 = x1 as Element of X1 by A4;
 a = [x1,x2,x3] by A3, A6;
hence  ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ; ::_thesis: verum
end;
given x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that A7: a = [x1,x2,x3] ; ::_thesis: a in [:X1,X2,X3:]
 a = [[x1,x2],x3] by A7;
then  a in [:[:X1,X2:],X3:] ;
hence  a in [:X1,X2,X3:] by ZFMISC_1:def_3; ::_thesis: verum
end;

theorem Th4: :: DOMAIN_1:4
for D, X1, X2, X3 being non empty set st ( for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) holds
D = [:X1,X2,X3:]
proof
let D, X1, X2, X3 be non empty set ; ::_thesis: ( ( for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) implies D = [:X1,X2,X3:] )
assume A1: for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ; ::_thesis: D = [:X1,X2,X3:]
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_D_implies_a_in_[:[:X1,X2:],X3:]_)_&_(_a_in_[:[:X1,X2:],X3:]_implies_a_in_D_)_)
let a be set ; ::_thesis: ( ( a in D implies a in [:[:X1,X2:],X3:] ) & ( a in [:[:X1,X2:],X3:] implies a in D ) )
thus  ( a in D implies a in [:[:X1,X2:],X3:] ) ::_thesis: ( a in [:[:X1,X2:],X3:] implies a in D )
proof
assume  a in D ; ::_thesis: a in [:[:X1,X2:],X3:]
then consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that
A2: a = [x1,x2,x3] by A1;
 a = [[x1,x2],x3] by A2;
hence  a in [:[:X1,X2:],X3:] ; ::_thesis: verum
end;
assume  a in [:[:X1,X2:],X3:] ; ::_thesis: a in D
then consider x12, x3 being set  such that
A3: x12 in [:X1,X2:] and
A4: x3 in X3 and
A5: a = [x12,x3] by ZFMISC_1:def_2;
reconsider x3 = x3 as Element of X3 by A4;
consider x1, x2 being set  such that
A6: x1 in X1 and
A7: x2 in X2 and
A8: x12 = [x1,x2] by A3, ZFMISC_1:def_2;
reconsider x2 = x2 as Element of X2 by A7;
reconsider x1 = x1 as Element of X1 by A6;
 a = [x1,x2,x3] by A5, A8;
hence  a in D by A1; ::_thesis: verum
end;
then  D = [:[:X1,X2:],X3:] by TARSKI:1;
hence  D = [:X1,X2,X3:] by ZFMISC_1:def_3; ::_thesis: verum
end;

theorem :: DOMAIN_1:5
for D, X1, X2, X3 being non empty set holds
( D = [:X1,X2,X3:] iff for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) by Th3, Th4;


definition
let X1, X2, X3 be non empty set ;
let x1 be Element of X1;
let x2 be Element of X2;
let x3 be Element of X3;
:: original: [
redefine func[x1,x2,x3] ->  Element of [:X1,X2,X3:];
coherence
 [x1,x2,x3] is Element of [:X1,X2,X3:] by MCART_1:69;
end;

theorem :: DOMAIN_1:6
for a being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( a = x `1_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 )
proof
let a be set ; ::_thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( a = x `1_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 )
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds
( a = x `1_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 )
let x be Element of [:X1,X2,X3:]; ::_thesis: ( a = x `1_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 )
thus  ( a = x `1_3 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 ) implies a = x `1_3 )
proof
A1: x = [(x `1_3),(x `2_3),(x `3_3)] ;
assume A2: a = x `1_3 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1
let x2 be Element of X2; ::_thesis: for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1
let x3 be Element of X3; ::_thesis: ( x = [x1,x2,x3] implies a = x1 )
assume  x = [x1,x2,x3] ; ::_thesis: a = x1
hence  a = x1 by A2, A1, XTUPLE_0:3; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 ) implies a = x `1_3 ) by MCART_1:65; ::_thesis: verum
end;

theorem :: DOMAIN_1:7
for b being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( b = x `2_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 )
proof
let b be set ; ::_thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( b = x `2_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 )
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds
( b = x `2_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 )
let x be Element of [:X1,X2,X3:]; ::_thesis: ( b = x `2_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 )
thus  ( b = x `2_3 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 ) implies b = x `2_3 )
proof
A1: x = [(x `1_3),(x `2_3),(x `3_3)] ;
assume A2: b = x `2_3 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2
let x2 be Element of X2; ::_thesis: for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2
let x3 be Element of X3; ::_thesis: ( x = [x1,x2,x3] implies b = x2 )
assume  x = [x1,x2,x3] ; ::_thesis: b = x2
hence  b = x2 by A2, A1, XTUPLE_0:3; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 ) implies b = x `2_3 ) by MCART_1:66; ::_thesis: verum
end;

theorem :: DOMAIN_1:8
for c being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( c = x `3_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 )
proof
let c be set ; ::_thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( c = x `3_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 )
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds
( c = x `3_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 )
let x be Element of [:X1,X2,X3:]; ::_thesis: ( c = x `3_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 )
thus  ( c = x `3_3 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 ) implies c = x `3_3 )
proof
A1: x = [(x `1_3),(x `2_3),(x `3_3)] ;
assume A2: c = x `3_3 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3
let x2 be Element of X2; ::_thesis: for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3
let x3 be Element of X3; ::_thesis: ( x = [x1,x2,x3] implies c = x3 )
assume  x = [x1,x2,x3] ; ::_thesis: c = x3
hence  c = x3 by A2, A1, XTUPLE_0:3; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 ) implies c = x `3_3 ) by MCART_1:67; ::_thesis: verum
end;

theorem :: DOMAIN_1:9
for X1, X2, X3 being non empty set
for x, y being Element of [:X1,X2,X3:] st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 holds
x = y
proof
let X1, X2, X3 be non empty set ; ::_thesis: for x, y being Element of [:X1,X2,X3:] st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 holds
x = y
let x, y be Element of [:X1,X2,X3:]; ::_thesis: ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 implies x = y )
 [(x `1_3),(x `2_3),(x `3_3)] = x ;
hence  ( x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 implies x = y ) by MCART_1:44; ::_thesis: verum
end;

theorem Th10: :: DOMAIN_1:10
for a being set
for X1, X2, X3, X4 being non empty set holds
( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )
proof
let a be set ; ::_thesis: for X1, X2, X3, X4 being non empty set holds
( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )
let X1, X2, X3, X4 be non empty set ; ::_thesis: ( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )
thus  ( a in [:X1,X2,X3,X4:] implies ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ::_thesis: ( ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] implies a in [:X1,X2,X3,X4:] )
proof
assume  a in [:X1,X2,X3,X4:] ; ::_thesis: ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4]
then  a 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: a = [x123,x4] by ZFMISC_1:def_2;
reconsider x4 = x4 as Element of X4 by A2;
consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that
A4: x123 = [x1,x2,x3] by A1, Th3;
 a = [x1,x2,x3,x4] by A3, A4;
hence  ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ; ::_thesis: verum
end;
given x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that A5: a = [x1,x2,x3,x4] ; ::_thesis: a in [:X1,X2,X3,X4:]
 a = [[x1,x2,x3],x4] by A5;
then  a in [:[:X1,X2,X3:],X4:] ;
hence  a in [:X1,X2,X3,X4:] by ZFMISC_1:def_4; ::_thesis: verum
end;

theorem Th11: :: DOMAIN_1:11
for D, X1, X2, X3, X4 being non empty set st ( for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) holds
D = [:X1,X2,X3,X4:]
proof
let D, X1, X2, X3, X4 be non empty set ; ::_thesis: ( ( for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) implies D = [:X1,X2,X3,X4:] )
assume A1: for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ; ::_thesis: D = [:X1,X2,X3,X4:]
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_D_implies_a_in_[:[:X1,X2,X3:],X4:]_)_&_(_a_in_[:[:X1,X2,X3:],X4:]_implies_a_in_D_)_)
let a be set ; ::_thesis: ( ( a in D implies a in [:[:X1,X2,X3:],X4:] ) & ( a in [:[:X1,X2,X3:],X4:] implies a in D ) )
thus  ( a in D implies a in [:[:X1,X2,X3:],X4:] ) ::_thesis: ( a in [:[:X1,X2,X3:],X4:] implies a in D )
proof
assume  a in D ; ::_thesis: a in [:[:X1,X2,X3:],X4:]
then consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that
A2: a = [x1,x2,x3,x4] by A1;
 a = [[x1,x2,x3],x4] by A2;
hence  a in [:[:X1,X2,X3:],X4:] ; ::_thesis: verum
end;
assume  a in [:[:X1,X2,X3:],X4:] ; ::_thesis: a in D
then consider x123, x4 being set  such that
A3: x123 in [:X1,X2,X3:] and
A4: x4 in X4 and
A5: a = [x123,x4] by ZFMISC_1:def_2;
reconsider x4 = x4 as Element of X4 by A4;
consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that
A6: x123 = [x1,x2,x3] by A3, Th3;
 a = [x1,x2,x3,x4] by A5, A6;
hence  a in D by A1; ::_thesis: verum
end;
then  D = [:[:X1,X2,X3:],X4:] by TARSKI:1;
hence  D = [:X1,X2,X3,X4:] by ZFMISC_1:def_4; ::_thesis: verum
end;

theorem :: DOMAIN_1:12
for D, X1, X2, X3, X4 being non empty set holds
( D = [:X1,X2,X3,X4:] iff for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) by Th10, Th11;

definition
let X1, X2, X3, X4 be non empty set ;
let x1 be Element of X1;
let x2 be Element of X2;
let x3 be Element of X3;
let x4 be Element of X4;
:: original: [
redefine func[x1,x2,x3,x4] ->  Element of [:X1,X2,X3,X4:];
coherence
 [x1,x2,x3,x4] is Element of [:X1,X2,X3,X4:] by MCART_1:80;
end;

theorem :: DOMAIN_1:13
for a being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( a = x `1_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 )
proof
let a be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( a = x `1_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 )
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds
( a = x `1_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 )
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( a = x `1_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 )
thus  ( a = x `1_4 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 ) implies a = x `1_4 )
proof
A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
assume A2: a = x `1_4 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1
let x2 be Element of X2; ::_thesis: for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1
let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1
let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies a = x1 )
assume  x = [x1,x2,x3,x4] ; ::_thesis: a = x1
hence  a = x1 by A2, A1, XTUPLE_0:5; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 ) implies a = x `1_4 ) by MCART_1:75; ::_thesis: verum
end;

theorem :: DOMAIN_1:14
for b being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( b = x `2_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 )
proof
let b be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( b = x `2_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 )
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds
( b = x `2_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 )
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( b = x `2_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 )
thus  ( b = x `2_4 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 ) implies b = x `2_4 )
proof
A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
assume A2: b = x `2_4 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2
let x2 be Element of X2; ::_thesis: for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2
let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2
let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies b = x2 )
assume  x = [x1,x2,x3,x4] ; ::_thesis: b = x2
hence  b = x2 by A2, A1, XTUPLE_0:5; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 ) implies b = x `2_4 ) by MCART_1:76; ::_thesis: verum
end;

theorem :: DOMAIN_1:15
for c being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( c = x `3_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 )
proof
let c be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( c = x `3_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 )
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds
( c = x `3_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 )
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( c = x `3_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 )
thus  ( c = x `3_4 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 ) implies c = x `3_4 )
proof
A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
assume A2: c = x `3_4 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3
let x2 be Element of X2; ::_thesis: for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3
let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3
let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies c = x3 )
assume  x = [x1,x2,x3,x4] ; ::_thesis: c = x3
hence  c = x3 by A2, A1, XTUPLE_0:5; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 ) implies c = x `3_4 ) by MCART_1:77; ::_thesis: verum
end;

theorem :: DOMAIN_1:16
for d being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
proof
let d be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( d = x `4_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )
thus  ( d = x `4_4 implies for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) ::_thesis: ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) implies d = x `4_4 )
proof
A1: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
assume A2: d = x `4_4 ; ::_thesis: for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x1 be Element of X1; ::_thesis: for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x2 be Element of X2; ::_thesis: for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x3 be Element of X3; ::_thesis: for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4
let x4 be Element of X4; ::_thesis: ( x = [x1,x2,x3,x4] implies d = x4 )
assume  x = [x1,x2,x3,x4] ; ::_thesis: d = x4
hence  d = x4 by A2, A1, XTUPLE_0:5; ::_thesis: verum
end;
thus  ( ( for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) implies d = x `4_4 ) by MCART_1:78; ::_thesis: verum
end;

theorem :: DOMAIN_1:17
for X1, X2, X3, X4 being non empty set
for x, y being Element of [:X1,X2,X3,X4:] st x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 holds
x = y
proof
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x, y being Element of [:X1,X2,X3,X4:] st x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 holds
x = y
let x, y be Element of [:X1,X2,X3,X4:]; ::_thesis: ( x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 implies x = y )
 [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] = x ;
hence  ( x `1_4 = y `1_4 & x `2_4 = y `2_4 & x `3_4 = y `3_4 & x `4_4 = y `4_4 implies x = y ) by MCART_1:56; ::_thesis: verum
end;


scheme :: DOMAIN_1:sch 1
Fraenkel1{ P1[ set ] } :
 for X1 being non empty set holds  {  x1 where x1 is Element of X1 : P1[x1]  }  is Subset of X1
proof
let X1 be non empty set ; ::_thesis:  {  x1 where x1 is Element of X1 : P1[x1]  }  is Subset of X1
  {  x1 where x1 is Element of X1 : P1[x1]  }  c= X1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : P1[x1]  }  or a in X1 )
assume  a in  {  x1 where x1 is Element of X1 : P1[x1]  }  ; ::_thesis: a in X1
then  ex x1 being Element of X1 st
( a = x1 & P1[x1] ) ;
hence  a in X1 ; ::_thesis: verum
end;
hence   {  x1 where x1 is Element of X1 : P1[x1]  }  is Subset of X1 ; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 2
Fraenkel2{ P1[ set , set ] } :
 for X1, X2 being non empty set holds  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  is Subset of [:X1,X2:]
proof
let X1, X2 be non empty set ; ::_thesis:  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  is Subset of [:X1,X2:]
  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  c= [:X1,X2:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  or a in [:X1,X2:] )
assume  a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  ; ::_thesis: a in [:X1,X2:]
then  ex x1 being Element of X1 ex x2 being Element of X2 st
( a = [x1,x2] & P1[x1,x2] ) ;
hence  a in [:X1,X2:] ; ::_thesis: verum
end;
hence   {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  is Subset of [:X1,X2:] ; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 3
Fraenkel3{ P1[ set , set , set ] } :
 for X1, X2, X3 being non empty set holds  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3]  }  is Subset of [:X1,X2,X3:]
proof
let X1, X2, X3 be non empty set ; ::_thesis:  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3]  }  is Subset of [:X1,X2,X3:]
  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3]  }  c= [:X1,X2,X3:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3]  }  or a in [:X1,X2,X3:] )
assume  a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3]  }  ; ::_thesis: a in [:X1,X2,X3:]
then  ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st
( a = [x1,x2,x3] & P1[x1,x2,x3] ) ;
hence  a in [:X1,X2,X3:] ; ::_thesis: verum
end;
hence   {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3]  }  is Subset of [:X1,X2,X3:] ; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 4
Fraenkel4{ P1[ set , set , set , set ] } :
 for X1, X2, X3, X4 being non empty set holds  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4]  }  is Subset of [:X1,X2,X3,X4:]
proof
let X1, X2, X3, X4 be non empty set ; ::_thesis:  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4]  }  is Subset of [:X1,X2,X3,X4:]
  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4]  }  c= [:X1,X2,X3,X4:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4]  }  or a in [:X1,X2,X3,X4:] )
assume  a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4]  }  ; ::_thesis: a in [:X1,X2,X3,X4:]
then  ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st
( a = [x1,x2,x3,x4] & P1[x1,x2,x3,x4] ) ;
hence  a in [:X1,X2,X3,X4:] ; ::_thesis: verum
end;
hence   {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4]  }  is Subset of [:X1,X2,X3,X4:] ; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 5
Fraenkel5{ P1[ set ], P2[ set ] } :
 for X1 being non empty set st ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) holds
{  y1 where y1 is Element of X1 : P1[y1]  }  c=  {  z1 where z1 is Element of X1 : P2[z1]  }
proof
let X1 be non empty set ; ::_thesis: ( ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) implies  {  y1 where y1 is Element of X1 : P1[y1]  }  c=  {  z1 where z1 is Element of X1 : P2[z1]  }  )
assume A1: for x1 being Element of X1 st P1[x1] holds
P2[x1] ; ::_thesis:  {  y1 where y1 is Element of X1 : P1[y1]  }  c=  {  z1 where z1 is Element of X1 : P2[z1]  }
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  y1 where y1 is Element of X1 : P1[y1]  }  or a in  {  z1 where z1 is Element of X1 : P2[z1]  }  )
assume  a in  {  x1 where x1 is Element of X1 : P1[x1]  }  ; ::_thesis: a in  {  z1 where z1 is Element of X1 : P2[z1]  }
then consider x1 being Element of X1 such that
A2: a = x1 and
A3: P1[x1] ;
 P2[x1] by A1, A3;
hence  a in  {  z1 where z1 is Element of X1 : P2[z1]  }  by A2; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 6
Fraenkel6{ P1[ set ], P2[ set ] } :
 for X1 being non empty set st ( for x1 being Element of X1 holds
( P1[x1] iff P2[x1] ) ) holds
{  y1 where y1 is Element of X1 : P1[y1]  }  =  {  z1 where z1 is Element of X1 : P2[z1]  }
proof
let X1 be non empty set ; ::_thesis: ( ( for x1 being Element of X1 holds
( P1[x1] iff P2[x1] ) ) implies  {  y1 where y1 is Element of X1 : P1[y1]  }  =  {  z1 where z1 is Element of X1 : P2[z1]  }  )
assume A1: for x1 being Element of X1 holds
( P1[x1] iff P2[x1] ) ; ::_thesis:  {  y1 where y1 is Element of X1 : P1[y1]  }  =  {  z1 where z1 is Element of X1 : P2[z1]  }
 for X1 being non empty set st ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) holds
{  y1 where y1 is Element of X1 : P1[y1]  }  c=  {  z1 where z1 is Element of X1 : P2[z1]  }  from DOMAIN_1:sch_5();
hence   {  y1 where y1 is Element of X1 : P1[y1]  }  c=  {  z1 where z1 is Element of X1 : P2[z1]  }  by A1; :: according to XBOOLE_0:def_10 ::_thesis:  {  z1 where z1 is Element of X1 : P2[z1]  }  c=  {  y1 where y1 is Element of X1 : P1[y1]  }
 for X1 being non empty set st ( for x1 being Element of X1 st P2[x1] holds
P1[x1] ) holds
{  y1 where y1 is Element of X1 : P2[y1]  }  c=  {  z1 where z1 is Element of X1 : P1[z1]  }  from DOMAIN_1:sch_5();
hence   {  z1 where z1 is Element of X1 : P2[z1]  }  c=  {  y1 where y1 is Element of X1 : P1[y1]  }  by A1; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 7
SubsetD{ F1() ->  non empty set , P1[ set ] } :
  {  d where d is Element of F1() : P1[d]  }  is Subset of F1()
proof
 for D being non empty set holds  {  d where d is Element of D : P1[d]  }  is Subset of D from DOMAIN_1:sch_1();
hence   {  d where d is Element of F1() : P1[d]  }  is Subset of F1() ; ::_thesis: verum
end;

theorem :: DOMAIN_1:18
for X1 being non empty set holds X1 =  {  x1 where x1 is Element of X1 : verum  }
proof
let X1 be non empty set ; ::_thesis: X1 =  {  x1 where x1 is Element of X1 : verum  }
defpred S1[ set ] means verum;
A1: for y1 being Element of X1 holds y1 in  {  x1 where x1 is Element of X1 : verum  }  ;
  {  x1 where x1 is Element of X1 : S1[x1]  }  is Subset of X1 from DOMAIN_1:sch_7();
hence  X1 =  {  x1 where x1 is Element of X1 : verum  }  by A1, SUBSET_1:28; ::_thesis: verum
end;

theorem :: DOMAIN_1:19
for X1, X2 being non empty set holds [:X1,X2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }
proof
let X1, X2 be non empty set ; ::_thesis: [:X1,X2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }
defpred S1[ set , set ] means verum;
A1: for x being Element of [:X1,X2:] holds x in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }
proof
let x be Element of [:X1,X2:]; ::_thesis: x in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }
 x = [(x `1),(x `2)] by MCART_1:21;
hence  x in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }  ; ::_thesis: verum
end;
 for X1, X2 being non empty set holds  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : S1[x1,x2]  }  is Subset of [:X1,X2:] from DOMAIN_1:sch_2();
then   {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }  is Subset of [:X1,X2:] ;
hence  [:X1,X2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum  }  by A1, SUBSET_1:28; ::_thesis: verum
end;

theorem :: DOMAIN_1:20
for X1, X2, X3 being non empty set holds [:X1,X2,X3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }
proof
let X1, X2, X3 be non empty set ; ::_thesis: [:X1,X2,X3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }
defpred S1[ set , set , set ] means verum;
A1: for x being Element of [:X1,X2,X3:] holds x in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }
proof
let x be Element of [:X1,X2,X3:]; ::_thesis: x in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }
 x = [(x `1_3),(x `2_3),(x `3_3)] ;
hence  x in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }  ; ::_thesis: verum
end;
 for X1, X2, X3 being non empty set holds  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : S1[x1,x2,x3]  }  is Subset of [:X1,X2,X3:] from DOMAIN_1:sch_3();
then   {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }  is Subset of [:X1,X2,X3:] ;
hence  [:X1,X2,X3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum  }  by A1, SUBSET_1:28; ::_thesis: verum
end;

theorem :: DOMAIN_1:21
for X1, X2, X3, X4 being non empty set holds [:X1,X2,X3,X4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }
proof
let X1, X2, X3, X4 be non empty set ; ::_thesis: [:X1,X2,X3,X4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }
defpred S1[ set , set , set , set ] means verum;
A1: for x being Element of [:X1,X2,X3,X4:] holds x in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }
proof
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: x in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }
 x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence  x in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }  ; ::_thesis: verum
end;
 for X1, X2, X3, X4 being non empty set holds  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : S1[x1,x2,x3,x4]  }  is Subset of [:X1,X2,X3,X4:] from DOMAIN_1:sch_4();
then   {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }  is Subset of [:X1,X2,X3,X4:] ;
hence  [:X1,X2,X3,X4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum  }  by A1, SUBSET_1:28; ::_thesis: verum
end;

theorem :: DOMAIN_1:22
for X1 being non empty set
for A1 being Subset of X1 holds A1 =  {  x1 where x1 is Element of X1 : x1 in A1  }
proof
let X1 be non empty set ; ::_thesis: for A1 being Subset of X1 holds A1 =  {  x1 where x1 is Element of X1 : x1 in A1  }
let A1 be Subset of X1; ::_thesis: A1 =  {  x1 where x1 is Element of X1 : x1 in A1  }
thus  A1 c=  {  x1 where x1 is Element of X1 : x1 in A1  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : x1 in A1  }  c= A1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in  {  x1 where x1 is Element of X1 : x1 in A1  }  )
assume  a in A1 ; ::_thesis: a in  {  x1 where x1 is Element of X1 : x1 in A1  }
hence  a in  {  x1 where x1 is Element of X1 : x1 in A1  }  ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : x1 in A1  }  or a in A1 )
assume  a in  {  x1 where x1 is Element of X1 : x1 in A1  }  ; ::_thesis: a in A1
then  ex x1 being Element of X1 st
( a = x1 & x1 in A1 ) ;
hence  a in A1 ; ::_thesis: verum
end;

theorem :: DOMAIN_1:23
for X1, X2 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2 holds [:A1,A2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }
proof
let X1, X2 be non empty set ; ::_thesis: for A1 being Subset of X1
for A2 being Subset of X2 holds [:A1,A2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }
let A1 be Subset of X1; ::_thesis: for A2 being Subset of X2 holds [:A1,A2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }
let A2 be Subset of X2; ::_thesis: [:A1,A2:] =  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }
thus  [:A1,A2:] c=  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }  c= [:A1,A2:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:A1,A2:] or a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }  )
assume A1: a in [:A1,A2:] ; ::_thesis: a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }
then reconsider x = a as Element of [:X1,X2:] ;
A2: x = [(x `1),(x `2)] by MCART_1:21;
 ( x `1 in A1 & x `2 in A2 ) by A1, MCART_1:10;
hence  a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }  by A2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }  or a in [:A1,A2:] )
assume  a in  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 )  }  ; ::_thesis: a in [:A1,A2:]
then  ex x1 being Element of X1 ex x2 being Element of X2 st
( a = [x1,x2] & x1 in A1 & x2 in A2 ) ;
hence  a in [:A1,A2:] by ZFMISC_1:87; ::_thesis: verum
end;

theorem :: DOMAIN_1:24
for X1, X2, X3 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3 holds [:A1,A2,A3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }
proof
let X1, X2, X3 be non empty set ; ::_thesis: for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3 holds [:A1,A2,A3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }
let A1 be Subset of X1; ::_thesis: for A2 being Subset of X2
for A3 being Subset of X3 holds [:A1,A2,A3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }
let A2 be Subset of X2; ::_thesis: for A3 being Subset of X3 holds [:A1,A2,A3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }
let A3 be Subset of X3; ::_thesis: [:A1,A2,A3:] =  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }
thus  [:A1,A2,A3:] c=  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }  c= [:A1,A2,A3:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:A1,A2,A3:] or a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }  )
assume B1: a in [:A1,A2,A3:] ; ::_thesis: a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }
reconsider A1 = A1 as non empty Subset of X1 by B1, MCART_1:31;
reconsider A2 = A2 as non empty Subset of X2 by B1, MCART_1:31;
reconsider A3 = A3 as non empty Subset of X3 by B1, MCART_1:31;
A1: a in [:A1,A2,A3:] by B1;
reconsider x = a as Element of [:X1,X2,X3:] by A1;
B2: x = [(x `1_3),(x `2_3),(x `3_3)] ;
A2: x `3_3 in A3 by A1, MCART_1:72;
 ( x `1_3 in A1 & x `2_3 in A2 ) by A1, MCART_1:72;
hence  a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }  by A2, B2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }  or a in [:A1,A2,A3:] )
assume  a in  {  [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 )  }  ; ::_thesis: a in [:A1,A2,A3:]
then  ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st
( a = [x1,x2,x3] & x1 in A1 & x2 in A2 & x3 in A3 ) ;
hence  a in [:A1,A2,A3:] by MCART_1:69; ::_thesis: verum
end;

theorem :: DOMAIN_1:25
for X1, X2, X3, X4 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
proof
let X1, X2, X3, X4 be non empty set ; ::_thesis: for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
let A1 be Subset of X1; ::_thesis: for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
let A2 be Subset of X2; ::_thesis: for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
let A3 be Subset of X3; ::_thesis: for A4 being Subset of X4 holds [:A1,A2,A3,A4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
let A4 be Subset of X4; ::_thesis: [:A1,A2,A3,A4:] =  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
thus  [:A1,A2,A3,A4:] c=  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }  c= [:A1,A2,A3,A4:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:A1,A2,A3,A4:] or a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }  )
assume B1: a in [:A1,A2,A3,A4:] ; ::_thesis: a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }
reconsider A1 = A1 as non empty Subset of X1 by B1, MCART_1:51;
reconsider A2 = A2 as non empty Subset of X2 by B1, MCART_1:51;
reconsider A3 = A3 as non empty Subset of X3 by B1, MCART_1:51;
reconsider A4 = A4 as non empty Subset of X4 by B1, MCART_1:51;
A1: a in [:A1,A2,A3,A4:] by B1;
then reconsider x = a as Element of [:X1,X2,X3,X4:] ;
A2: ( x `3_4 in A3 & x `4_4 in A4 ) by A1, MCART_1:83;
A3: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
 ( x `1_4 in A1 & x `2_4 in A2 ) by A1, MCART_1:83;
hence  a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }  by A3, A2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }  or a in [:A1,A2,A3,A4:] )
assume  a in  {  [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 )  }  ; ::_thesis: a in [:A1,A2,A3,A4:]
then  ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st
( a = [x1,x2,x3,x4] & x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) ;
hence  a in [:A1,A2,A3,A4:] by MCART_1:80; ::_thesis: verum
end;

theorem :: DOMAIN_1:26
for X1 being non empty set holds {} X1 =  {  x1 where x1 is Element of X1 : contradiction  }
proof
let X1 be non empty set ; ::_thesis: {} X1 =  {  x1 where x1 is Element of X1 : contradiction  }
thus  {} X1 c=  {  x1 where x1 is Element of X1 : contradiction  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : contradiction  }  c= {} X1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {} X1 or a in  {  x1 where x1 is Element of X1 : contradiction  }  )
thus  ( not a in {} X1 or a in  {  x1 where x1 is Element of X1 : contradiction  }  ) ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : contradiction  }  or a in {} X1 )
assume  a in  {  x1 where x1 is Element of X1 : contradiction  }  ; ::_thesis: a in {} X1
then  ex x1 being Element of X1 st
( a = x1 & contradiction ) ;
hence  a in {} X1 ; ::_thesis: verum
end;

theorem :: DOMAIN_1:27
for X1 being non empty set
for A1 being Subset of X1 holds A1 ` =  {  x1 where x1 is Element of X1 : not x1 in A1  }
proof
let X1 be non empty set ; ::_thesis: for A1 being Subset of X1 holds A1 ` =  {  x1 where x1 is Element of X1 : not x1 in A1  }
let A1 be Subset of X1; ::_thesis: A1 ` =  {  x1 where x1 is Element of X1 : not x1 in A1  }
thus  A1 ` c=  {  x1 where x1 is Element of X1 : not x1 in A1  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : not x1 in A1  }  c= A1 `
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 ` or a in  {  x1 where x1 is Element of X1 : not x1 in A1  }  )
assume A1: a in A1 ` ; ::_thesis: a in  {  x1 where x1 is Element of X1 : not x1 in A1  }
then  not a in A1 by XBOOLE_0:def_5;
hence  a in  {  x1 where x1 is Element of X1 : not x1 in A1  }  by A1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : not x1 in A1  }  or a in A1 ` )
assume  a in  {  x1 where x1 is Element of X1 : not x1 in A1  }  ; ::_thesis: a in A1 `
then  ex x1 being Element of X1 st
( a = x1 & not x1 in A1 ) ;
hence  a in A1 ` by SUBSET_1:29; ::_thesis: verum
end;

theorem :: DOMAIN_1:28
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 /\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 /\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }
let A1, B1 be Subset of X1; ::_thesis: A1 /\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }
thus  A1 /\ B1 c=  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }  c= A1 /\ B1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 /\ B1 or a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }  )
assume A1: a in A1 /\ B1 ; ::_thesis: a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }
then reconsider x = a as Element of X1 ;
 ( x in A1 & x in B1 ) by A1, XBOOLE_0:def_4;
hence  a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }  ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }  or a in A1 /\ B1 )
assume  a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 )  }  ; ::_thesis: a in A1 /\ B1
then  ex x1 being Element of X1 st
( a = x1 & x1 in A1 & x1 in B1 ) ;
hence  a in A1 /\ B1 by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: DOMAIN_1:29
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \/ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \/ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }
let A1, B1 be Subset of X1; ::_thesis: A1 \/ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }
thus  A1 \/ B1 c=  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }  c= A1 \/ B1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 \/ B1 or a in  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }  )
assume A1: a in A1 \/ B1 ; ::_thesis: a in  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }
then reconsider x = a as Element of X1 ;
 ( x in A1 or x in B1 ) by A1, XBOOLE_0:def_3;
hence  a in  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }  ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }  or a in A1 \/ B1 )
assume  a in  {  x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 )  }  ; ::_thesis: a in A1 \/ B1
then  ex x1 being Element of X1 st
( a = x1 & ( x1 in A1 or x1 in B1 ) ) ;
hence  a in A1 \/ B1 by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: DOMAIN_1:30
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }
let A1, B1 be Subset of X1; ::_thesis: A1 \ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }
thus  A1 \ B1 c=  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }  c= A1 \ B1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 \ B1 or a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }  )
assume A1: a in A1 \ B1 ; ::_thesis: a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }
then reconsider x = a as Element of X1 ;
 ( x in A1 & not x in B1 ) by A1, XBOOLE_0:def_5;
hence  a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }  ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }  or a in A1 \ B1 )
assume  a in  {  x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 )  }  ; ::_thesis: a in A1 \ B1
then  ex x1 being Element of X1 st
( a = x1 & x1 in A1 & not x1 in B1 ) ;
hence  a in A1 \ B1 by XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th31: :: DOMAIN_1:31
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }
let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }
thus  A1 \+\ B1 c=  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  c= A1 \+\ B1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 \+\ B1 or a in  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  )
assume A1: a in A1 \+\ B1 ; ::_thesis: a in  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }
then reconsider x = a as Element of X1 ;
 ( ( x in A1 & not x in B1 ) or ( not x in A1 & x in B1 ) ) by A1, XBOOLE_0:1;
hence  a in  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  or a in A1 \+\ B1 )
assume  a in  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  ; ::_thesis: a in A1 \+\ B1
then  ex x1 being Element of X1 st
( a = x1 & ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) ) ;
hence  a in A1 \+\ B1 by XBOOLE_0:1; ::_thesis: verum
end;

theorem Th32: :: DOMAIN_1:32
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 )  }
let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 )  }
A1: for x1 being Element of X1 holds
( ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) iff ( not x1 in A1 iff x1 in B1 ) ) ;
defpred S1[ set ] means ( not $1 in A1 iff $1 in B1 );
defpred S2[ set ] means ( ( $1 in A1 & not $1 in B1 ) or ( not $1 in A1 & $1 in B1 ) );
A2: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) )  }  by Th31;
 for X1 being non empty set st ( for x1 being Element of X1 holds
( S2[x1] iff S1[x1] ) ) holds
{  y1 where y1 is Element of X1 : S2[y1]  }  =  {  z1 where z1 is Element of X1 : S1[z1]  }  from DOMAIN_1:sch_6();
hence  A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 )  }  by A1, A2; ::_thesis: verum
end;

theorem :: DOMAIN_1:33
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 )  }
let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 )  }
A1: for x1 being Element of X1 holds
(  not ( ( not x1 in A1 implies x1 in B1 ) & ( x1 in B1 implies not x1 in A1 ) & not ( x1 in A1 iff not x1 in B1 ) ) & not ( ( x1 in A1 implies not x1 in B1 ) & ( not x1 in B1 implies x1 in A1 ) & not ( not x1 in A1 iff x1 in B1 ) ) ) ;
defpred S1[ set ] means ( $1 in A1 iff not $1 in B1 );
defpred S2[ set ] means ( not $1 in A1 iff $1 in B1 );
A2: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 )  }  by Th32;
 for X1 being non empty set st ( for x1 being Element of X1 holds
( S2[x1] iff S1[x1] ) ) holds
{  y1 where y1 is Element of X1 : S2[y1]  }  =  {  z1 where z1 is Element of X1 : S1[z1]  }  from DOMAIN_1:sch_6();
hence  A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 )  }  by A1, A2; ::_thesis: verum
end;

theorem :: DOMAIN_1:34
for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) )  }
proof
let X1 be non empty set ; ::_thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) )  }
let A1, B1 be Subset of X1; ::_thesis: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) )  }
A1: for x1 being Element of X1 holds
( ( not x1 in A1 iff x1 in B1 ) iff ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) ) ;
defpred S1[ set ] means ( ( $1 in A1 & not $1 in B1 ) or ( $1 in B1 & not $1 in A1 ) );
defpred S2[ set ] means ( not $1 in A1 iff $1 in B1 );
A2: A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 )  }  by Th32;
 for X1 being non empty set st ( for x1 being Element of X1 holds
( S2[x1] iff S1[x1] ) ) holds
{  y1 where y1 is Element of X1 : S2[y1]  }  =  {  z1 where z1 is Element of X1 : S1[z1]  }  from DOMAIN_1:sch_6();
hence  A1 \+\ B1 =  {  x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) )  }  by A1, A2; ::_thesis: verum
end;

definition
let D be non empty set ;
let x1 be Element of D;
:: original: {
redefine func{x1} ->  Subset of D;
coherence
 {x1} is Subset of D by SUBSET_1:33;
let x2 be Element of D;
:: original: {
redefine func{x1,x2} ->  Subset of D;
coherence
 {x1,x2} is Subset of D by SUBSET_1:34;
let x3 be Element of D;
:: original: {
redefine func{x1,x2,x3} ->  Subset of D;
coherence
 {x1,x2,x3} is Subset of D by SUBSET_1:35;
let x4 be Element of D;
:: original: {
redefine func{x1,x2,x3,x4} ->  Subset of D;
coherence
 {x1,x2,x3,x4} is Subset of D by SUBSET_1:36;
let x5 be Element of D;
:: original: {
redefine func{x1,x2,x3,x4,x5} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5} is Subset of D by SUBSET_1:37;
let x6 be Element of D;
:: original: {
redefine func{x1,x2,x3,x4,x5,x6} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5,x6} is Subset of D by SUBSET_1:38;
let x7 be Element of D;
:: original: {
redefine func{x1,x2,x3,x4,x5,x6,x7} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5,x6,x7} is Subset of D by SUBSET_1:39;
let x8 be Element of D;
:: original: {
redefine func{x1,x2,x3,x4,x5,x6,x7,x8} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of D by SUBSET_1:40;
end;

begin

scheme :: DOMAIN_1:sch 8
SubsetFD{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  Element of F2(), P1[ set ] } :
  {  F3(x) where x is Element of F1() : P1[x]  }  is Subset of F2()
proof
set X =  {  F3(x) where x is Element of F1() : P1[x]  }  ;
  {  F3(x) where x is Element of F1() : P1[x]  }  c= F2()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  F3(x) where x is Element of F1() : P1[x]  }  or y in F2() )
assume  y in  {  F3(x) where x is Element of F1() : P1[x]  }  ; ::_thesis: y in F2()
then  ex z being Element of F1() st
( y = F3(z) & P1[z] ) ;
hence  y in F2() ; ::_thesis: verum
end;
hence   {  F3(x) where x is Element of F1() : P1[x]  }  is Subset of F2() ; ::_thesis: verum
end;

scheme :: DOMAIN_1:sch 9
SubsetFD2{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set , set ) ->  Element of F3(), P1[ set , set ] } :
  {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  is Subset of F3()
proof
set X =  {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  ;
  {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  c= F3()
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in  {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  or w in F3() )
assume  w in  {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  ; ::_thesis: w in F3()
then  ex x being Element of F1() ex y being Element of F2() st
( w = F4(x,y) & P1[x,y] ) ;
hence  w in F3() ; ::_thesis: verum
end;
hence   {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  is Subset of F3() ; ::_thesis: verum
end;

definition
let D1, D2, D3 be non empty set ;
let x be Element of [:[:D1,D2:],D3:];
:: original: `11
redefine funcx `11  ->  Element of D1;
coherence
 x `11 is Element of D1
proof
 x `11 = (x `1) `1 by MCART_1:def_14;
hence  x `11 is Element of D1 ; ::_thesis: verum
end;
:: original: `12
redefine funcx `12  ->  Element of D2;
coherence
 x `12 is Element of D2
proof
 x `12 = (x `1) `2 by MCART_1:def_15;
hence  x `12 is Element of D2 ; ::_thesis: verum
end;
end;

definition
let D1, D2, D3 be non empty set ;
let x be Element of [:D1,[:D2,D3:]:];
:: original: `21
redefine funcx `21  ->  Element of D2;
coherence
 x `21 is Element of D2
proof
 x `21 = (x `2) `1 by MCART_1:def_16;
hence  x `21 is Element of D2 ; ::_thesis: verum
end;
:: original: `22
redefine funcx `22  ->  Element of D3;
coherence
 x `22 is Element of D3
proof
 x `22 = (x `2) `2 by MCART_1:def_17;
hence  x `22 is Element of D3 ; ::_thesis: verum
end;
end;

scheme :: DOMAIN_1:sch 10
AndScheme{ F1() ->  non empty set , P1[ set ], P2[ set ] } :
  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  =  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }
proof
set A =  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  ;
set A1 =  {  a1 where a1 is Element of F1() : P1[a1]  }  ;
set A2 =  {  a2 where a2 is Element of F1() : P2[a2]  }  ;
thus   {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  c=  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }  c=  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  or x in  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }  )
assume  x in  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  ; ::_thesis: x in  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }
then consider a being Element of F1() such that
A1: x = a and
A2: ( P1[a] & P2[a] ) ;
 ( a in  {  a1 where a1 is Element of F1() : P1[a1]  }  & a in  {  a2 where a2 is Element of F1() : P2[a2]  }  ) by A2;
hence  x in  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }  by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }  or x in  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  )
assume A3: x in  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }  ; ::_thesis: x in  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }
then  x in  {  a2 where a2 is Element of F1() : P2[a2]  }  by XBOOLE_0:def_4;
then A4: ex a being Element of F1() st
( x = a & P2[a] ) ;
 x in  {  a1 where a1 is Element of F1() : P1[a1]  }  by A3, XBOOLE_0:def_4;
then  ex a being Element of F1() st
( x = a & P1[a] ) ;
hence  x in  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  by A4; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster non empty c=-linear for Element of bool A;
existence
 ex b1 being Subset of A st
( b1 is c=-linear & not b1 is empty )
proof
set a = the Element of A;
reconsider B = { the Element of A} as non empty Subset of A ;
take  B ; ::_thesis: ( B is c=-linear & not B is empty )
 B is c=-linear
proof
let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not x in B or not y in B or x,y are_c=-comparable )
assume that
A1: x in B and
A2: y in B ; ::_thesis: x,y are_c=-comparable
 x = the Element of A by A1, TARSKI:def_1;
hence  x,y are_c=-comparable by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  ( B is c=-linear & not B is empty ) ; ::_thesis: verum
end;
end;