:: by Andrzej Trybulec

::

:: Received April 3, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: DOMAIN_1:1

canceled;

theorem :: DOMAIN_1:2

canceled;

theorem :: DOMAIN_1:3

canceled;

theorem :: DOMAIN_1:4

canceled;

theorem :: DOMAIN_1:5

canceled;

theorem :: DOMAIN_1:6

canceled;

theorem :: DOMAIN_1:7

canceled;

theorem :: DOMAIN_1:8

canceled;

theorem :: DOMAIN_1:9

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]

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 end;

theorem :: DOMAIN_1:10

canceled;

theorem :: DOMAIN_1:11

canceled;

theorem :: DOMAIN_1:12

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

for x, y being Element of [:X1,X2:] st x `1 = y `1 & x `2 = y `2 holds

x = y

proof 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:106;

end;
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:106;

definition

let X1, X2 be non empty set ;

let x be Element of [:X1,X2:];

:: original: `1

redefine func x `1 -> Element of X1;

coherence

x `1 is Element of X1 by MCART_1:10;

:: original: `2

redefine func x `2 -> Element of X2;

coherence

x `2 is Element of X2 by MCART_1:10;

end;
let x be Element of [:X1,X2:];

:: original: `1

redefine func x `1 -> Element of X1;

coherence

x `1 is Element of X1 by MCART_1:10;

:: original: `2

redefine func x `2 -> Element of X2;

coherence

x `2 is Element of X2 by MCART_1:10;

theorem :: DOMAIN_1:13

canceled;

theorem :: DOMAIN_1:14

canceled;

theorem Th15: :: DOMAIN_1:15

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] )

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 end;

theorem Th16: :: DOMAIN_1:16

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:]

( 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 end;

theorem :: DOMAIN_1:17

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 Th15, Th16;

( 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 Th15, Th16;

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:73;

end;
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:73;

theorem :: DOMAIN_1:18

canceled;

theorem :: DOMAIN_1:19

canceled;

theorem :: DOMAIN_1:20

canceled;

theorem :: DOMAIN_1:21

canceled;

theorem :: DOMAIN_1:22

canceled;

theorem :: DOMAIN_1:23

canceled;

theorem :: DOMAIN_1:24

for a being set

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( a = x `1 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 )

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( a = x `1 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 end;

theorem :: DOMAIN_1:25

for b being set

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( b = x `2 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 )

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( b = x `2 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 end;

theorem :: DOMAIN_1:26

for c being set

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( c = x `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 )

for X1, X2, X3 being non empty set

for x being Element of [:X1,X2,X3:] holds

( c = x `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 end;

theorem :: DOMAIN_1:27

canceled;

theorem :: DOMAIN_1:28

for X1, X2, X3 being non empty set

for x, y being Element of [:X1,X2,X3:] st x `1 = y `1 & x `2 = y `2 & x `3 = y `3 holds

x = y

for x, y being Element of [:X1,X2,X3:] st x `1 = y `1 & x `2 = y `2 & x `3 = y `3 holds

x = y

proof end;

theorem :: DOMAIN_1:29

canceled;

theorem :: DOMAIN_1:30

canceled;

theorem Th31: :: DOMAIN_1:31

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] )

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 end;

theorem Th32: :: DOMAIN_1:32

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:]

( 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 end;

theorem :: DOMAIN_1:33

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 Th31, Th32;

( 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 Th31, Th32;

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:84;

end;
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:84;

theorem :: DOMAIN_1:34

canceled;

theorem :: DOMAIN_1:35

canceled;

theorem :: DOMAIN_1:36

canceled;

theorem :: DOMAIN_1:37

canceled;

theorem :: DOMAIN_1:38

canceled;

theorem :: DOMAIN_1:39

canceled;

theorem :: DOMAIN_1:40

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 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 )

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] holds

( a = x `1 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 end;

theorem :: DOMAIN_1:41

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 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 )

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] holds

( b = x `2 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 end;

theorem :: DOMAIN_1:42

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 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 )

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] holds

( c = x `3 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 end;

theorem :: DOMAIN_1:43

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 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 )

for X1, X2, X3, X4 being non empty set

for x being Element of [:X1,X2,X3,X4:] holds

( d = x `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 end;

theorem :: DOMAIN_1:44

canceled;

theorem :: DOMAIN_1:45

for X1, X2, X3, X4 being non empty set

for x, y being Element of [:X1,X2,X3,X4:] st x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 holds

x = y

for x, y being Element of [:X1,X2,X3,X4:] st x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 holds

x = y

proof end;

scheme :: DOMAIN_1:sch 2

Fraenkel2{ P_{1}[ set , set ] } :

Fraenkel2{ P

for X1, X2 being non empty set holds { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P_{1}[x1,x2] } is Subset of [:X1,X2:]

proof end;

scheme :: DOMAIN_1:sch 3

Fraenkel3{ P_{1}[ set , set , set ] } :

Fraenkel3{ P

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 : P_{1}[x1,x2,x3] } is Subset of [:X1,X2,X3:]

proof end;

scheme :: DOMAIN_1:sch 4

Fraenkel4{ P_{1}[ set , set , set , set ] } :

Fraenkel4{ P

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 : P_{1}[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:]

proof end;

scheme :: DOMAIN_1:sch 5

Fraenkel5{ P_{1}[ set ], P_{2}[ set ] } :

Fraenkel5{ P

for X1 being non empty set st ( for x1 being Element of X1 st P_{1}[x1] holds

P_{2}[x1] ) holds

{ y1 where y1 is Element of X1 : P_{1}[y1] } c= { z1 where z1 is Element of X1 : P_{2}[z1] }

P

{ y1 where y1 is Element of X1 : P

proof end;

scheme :: DOMAIN_1:sch 6

Fraenkel6{ P_{1}[ set ], P_{2}[ set ] } :

Fraenkel6{ P

for X1 being non empty set st ( for x1 being Element of X1 holds

( P_{1}[x1] iff P_{2}[x1] ) ) holds

{ y1 where y1 is Element of X1 : P_{1}[y1] } = { z1 where z1 is Element of X1 : P_{2}[z1] }

( P

{ y1 where y1 is Element of X1 : P

proof end;

theorem :: DOMAIN_1:46

canceled;

theorem :: DOMAIN_1:47

canceled;

theorem :: DOMAIN_1:48

proof end;

theorem :: DOMAIN_1:49

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 end;

theorem :: DOMAIN_1:50

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 end;

theorem :: DOMAIN_1:51

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 end;

theorem :: DOMAIN_1:52

for X1 being non empty set

for A1 being Subset of X1 holds A1 = { x1 where x1 is Element of X1 : x1 in A1 }

for A1 being Subset of X1 holds A1 = { x1 where x1 is Element of X1 : x1 in A1 }

proof end;

theorem :: DOMAIN_1:53

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 ) }

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 end;

theorem :: DOMAIN_1:54

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 ) }

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 end;

theorem :: DOMAIN_1:55

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 ) }

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 end;

theorem :: DOMAIN_1:56

proof end;

theorem :: DOMAIN_1:57

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 }

for A1 being Subset of X1 holds A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 }

proof end;

theorem :: DOMAIN_1:58

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 ) }

for A1, B1 being Subset of X1 holds A1 /\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) }

proof end;

theorem :: DOMAIN_1:59

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 ) }

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 end;

theorem :: DOMAIN_1:60

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 ) }

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 end;

theorem Th61: :: DOMAIN_1:61

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 ) ) }

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 end;

theorem Th62: :: DOMAIN_1:62

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 ) }

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 end;

theorem :: DOMAIN_1:63

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 ) }

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 end;

theorem :: DOMAIN_1:64

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 ) ) }

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 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:55;

let x2 be Element of D;

:: original: {

redefine func {x1,x2} -> Subset of D;

coherence

{x1,x2} is Subset of D by SUBSET_1:56;

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:57;

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:58;

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:59;

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:60;

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:61;

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:62;

end;
let x1 be Element of D;

:: original: {

redefine func {x1} -> Subset of D;

coherence

{x1} is Subset of D by SUBSET_1:55;

let x2 be Element of D;

:: original: {

redefine func {x1,x2} -> Subset of D;

coherence

{x1,x2} is Subset of D by SUBSET_1:56;

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:57;

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:58;

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:59;

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:60;

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:61;

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:62;

begin

scheme :: DOMAIN_1:sch 8

SubsetFD{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), P_{1}[ set ] } :

SubsetFD{ F

proof end;

scheme :: DOMAIN_1:sch 9

SubsetFD2{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( set , set ) -> Element of F_{3}(), P_{1}[ set , set ] } :

SubsetFD2{ F

{ F_{4}(x,y) where x is Element of F_{1}(), y is Element of F_{2}() : P_{1}[x,y] } is Subset of F_{3}()

proof end;

definition

let D1, D2, D3 be non empty set ;

let x be Element of [:[:D1,D2:],D3:];

:: original: `11

redefine func x `11 -> Element of D1;

coherence

x `11 is Element of D1

redefine func x `12 -> Element of D2;

coherence

x `12 is Element of D2

end;
let x be Element of [:[:D1,D2:],D3:];

:: original: `11

redefine func x `11 -> Element of D1;

coherence

x `11 is Element of D1

proof end;

:: original: `12redefine func x `12 -> Element of D2;

coherence

x `12 is Element of D2

proof end;

definition

let D1, D2, D3 be non empty set ;

let x be Element of [:D1,[:D2,D3:]:];

:: original: `21

redefine func x `21 -> Element of D2;

coherence

x `21 is Element of D2

redefine func x `22 -> Element of D3;

coherence

x `22 is Element of D3

end;
let x be Element of [:D1,[:D2,D3:]:];

:: original: `21

redefine func x `21 -> Element of D2;

coherence

x `21 is Element of D2

proof end;

:: original: `22redefine func x `22 -> Element of D3;

coherence

x `22 is Element of D3

proof end;

scheme :: DOMAIN_1:sch 10

AndScheme{ F_{1}() -> non empty set , P_{1}[ set ], P_{2}[ set ] } :

AndScheme{ F

{ a where a is Element of F_{1}() : ( P_{1}[a] & P_{2}[a] ) } = { a1 where a1 is Element of F_{1}() : P_{1}[a1] } /\ { a2 where a2 is Element of F_{1}() : P_{2}[a2] }

proof end;