:: by Andrzej Trybulec

::

:: Received September 4, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: FUNCOP_1:1

canceled;

theorem Th2: :: FUNCOP_1:2

proof end;

definition

let f be Function;

func f ~ -> Function means :Def1: :: FUNCOP_1:def 1

( dom it = dom f & ( for x being set st x in dom f holds

( ( for y, z being set st f . x = [y,z] holds

it . x = [z,y] ) & ( f . x = it . x or ex y, z being set st f . x = [y,z] ) ) ) );

existence

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom f holds

( ( for y, z being set st f . x = [y,z] holds

b_{1} . x = [z,y] ) & ( f . x = b_{1} . x or ex y, z being set st f . x = [y,z] ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom f holds

( ( for y, z being set st f . x = [y,z] holds

b_{1} . x = [z,y] ) & ( f . x = b_{1} . x or ex y, z being set st f . x = [y,z] ) ) ) & dom b_{2} = dom f & ( for x being set st x in dom f holds

( ( for y, z being set st f . x = [y,z] holds

b_{2} . x = [z,y] ) & ( f . x = b_{2} . x or ex y, z being set st f . x = [y,z] ) ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Function st dom b_{1} = dom b_{2} & ( for x being set st x in dom b_{2} holds

( ( for y, z being set st b_{2} . x = [y,z] holds

b_{1} . x = [z,y] ) & ( b_{2} . x = b_{1} . x or ex y, z being set st b_{2} . x = [y,z] ) ) ) holds

( dom b_{2} = dom b_{1} & ( for x being set st x in dom b_{1} holds

( ( for y, z being set st b_{1} . x = [y,z] holds

b_{2} . x = [z,y] ) & ( b_{1} . x = b_{2} . x or ex y, z being set st b_{1} . x = [y,z] ) ) ) )

end;
func f ~ -> Function means :Def1: :: FUNCOP_1:def 1

( dom it = dom f & ( for x being set st x in dom f holds

( ( for y, z being set st f . x = [y,z] holds

it . x = [z,y] ) & ( f . x = it . x or ex y, z being set st f . x = [y,z] ) ) ) );

existence

ex b

( dom b

( ( for y, z being set st f . x = [y,z] holds

b

proof end;

uniqueness for b

( ( for y, z being set st f . x = [y,z] holds

b

( ( for y, z being set st f . x = [y,z] holds

b

b

proof end;

involutiveness for b

( ( for y, z being set st b

b

( dom b

( ( for y, z being set st b

b

proof end;

:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :

for f, b

( b

( ( for y, z being set st f . x = [y,z] holds

b

theorem :: FUNCOP_1:3

canceled;

theorem :: FUNCOP_1:4

canceled;

theorem :: FUNCOP_1:5

canceled;

theorem Th6: :: FUNCOP_1:6

proof end;

theorem Th7: :: FUNCOP_1:7

proof end;

theorem :: FUNCOP_1:8

canceled;

theorem :: FUNCOP_1:9

proof end;

theorem Th10: :: FUNCOP_1:10

proof end;

theorem Th11: :: FUNCOP_1:11

proof end;

definition
end;

:: deftheorem defines --> FUNCOP_1:def 2 :

for A, z being set holds A --> z = [:A,{z}:];

registration

let A, z be set ;

cluster A --> z -> Relation-like Function-like ;

coherence

( A --> z is Function-like & A --> z is Relation-like )

end;
cluster A --> z -> Relation-like Function-like ;

coherence

( A --> z is Function-like & A --> z is Relation-like )

proof end;

theorem :: FUNCOP_1:12

canceled;

theorem Th13: :: FUNCOP_1:13

proof end;

theorem Th14: :: FUNCOP_1:14

theorem Th15: :: FUNCOP_1:15

proof end;

registration
end;

registration
end;

registration

let x be set ;

let A be non empty set ;

cluster A --> x -> non empty ;

coherence

not A --> x is empty ;

end;
let A be non empty set ;

cluster A --> x -> non empty ;

coherence

not A --> x is empty ;

theorem :: FUNCOP_1:16

theorem Th17: :: FUNCOP_1:17

for f being Function

for x being set st ( for z being set st z in dom f holds

f . z = x ) holds

f = (dom f) --> x

for x being set st ( for z being set st z in dom f holds

f . z = x ) holds

f = (dom f) --> x

proof end;

theorem Th18: :: FUNCOP_1:18

proof end;

theorem Th19: :: FUNCOP_1:19

proof end;

theorem Th20: :: FUNCOP_1:20

proof end;

theorem :: FUNCOP_1:21

proof end;

theorem :: FUNCOP_1:22

proof end;

theorem :: FUNCOP_1:23

proof end;

theorem :: FUNCOP_1:24

proof end;

theorem :: FUNCOP_1:25

proof end;

theorem :: FUNCOP_1:26

proof end;

definition

let F, f, g be Function;

func F .: (f,g) -> set equals :: FUNCOP_1:def 3

F * <:f,g:>;

correctness

coherence

F * <:f,g:> is set ;

;

end;
func F .: (f,g) -> set equals :: FUNCOP_1:def 3

F * <:f,g:>;

correctness

coherence

F * <:f,g:> is set ;

;

:: deftheorem defines .: FUNCOP_1:def 3 :

for F, f, g being Function holds F .: (f,g) = F * <:f,g:>;

registration

let F, f, g be Function;

cluster F .: (f,g) -> Relation-like Function-like ;

coherence

( F .: (f,g) is Function-like & F .: (f,g) is Relation-like ) ;

end;
cluster F .: (f,g) -> Relation-like Function-like ;

coherence

( F .: (f,g) is Function-like & F .: (f,g) is Relation-like ) ;

Lm1: for f, g, F being Function

for x being set st x in dom (F * <:f,g:>) holds

(F * <:f,g:>) . x = F . ((f . x),(g . x))

proof end;

theorem :: FUNCOP_1:27

for f, g, F, h being Function st dom h = dom (F .: (f,g)) & ( for z being set st z in dom (F .: (f,g)) holds

h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

proof end;

theorem :: FUNCOP_1:28

for f, g, F being Function

for x being set st x in dom (F .: (f,g)) holds

(F .: (f,g)) . x = F . ((f . x),(g . x)) by Lm1;

for x being set st x in dom (F .: (f,g)) holds

(F .: (f,g)) . x = F . ((f . x),(g . x)) by Lm1;

theorem Th29: :: FUNCOP_1:29

for f, g, h being Function

for A being set

for F being Function st f | A = g | A holds

(F .: (f,h)) | A = (F .: (g,h)) | A

for A being set

for F being Function st f | A = g | A holds

(F .: (f,h)) | A = (F .: (g,h)) | A

proof end;

theorem Th30: :: FUNCOP_1:30

for f, g, h being Function

for A being set

for F being Function st f | A = g | A holds

(F .: (h,f)) | A = (F .: (h,g)) | A

for A being set

for F being Function st f | A = g | A holds

(F .: (h,f)) | A = (F .: (h,g)) | A

proof end;

theorem Th31: :: FUNCOP_1:31

proof end;

definition

let F, f be Function;

let x be set ;

func F [:] (f,x) -> set equals :: FUNCOP_1:def 4

F * <:f,((dom f) --> x):>;

correctness

coherence

F * <:f,((dom f) --> x):> is set ;

;

end;
let x be set ;

func F [:] (f,x) -> set equals :: FUNCOP_1:def 4

F * <:f,((dom f) --> x):>;

correctness

coherence

F * <:f,((dom f) --> x):> is set ;

;

:: deftheorem defines [:] FUNCOP_1:def 4 :

for F, f being Function

for x being set holds F [:] (f,x) = F * <:f,((dom f) --> x):>;

registration

let F, f be Function;

let x be set ;

cluster F [:] (f,x) -> Relation-like Function-like ;

coherence

( F [:] (f,x) is Function-like & F [:] (f,x) is Relation-like ) ;

end;
let x be set ;

cluster F [:] (f,x) -> Relation-like Function-like ;

coherence

( F [:] (f,x) is Function-like & F [:] (f,x) is Relation-like ) ;

theorem :: FUNCOP_1:32

canceled;

theorem :: FUNCOP_1:33

canceled;

theorem :: FUNCOP_1:34

theorem Th35: :: FUNCOP_1:35

for f, F being Function

for x, z being set st x in dom (F [:] (f,z)) holds

(F [:] (f,z)) . x = F . ((f . x),z)

for x, z being set st x in dom (F [:] (f,z)) holds

(F [:] (f,z)) . x = F . ((f . x),z)

proof end;

theorem :: FUNCOP_1:36

for f, g being Function

for A being set

for F being Function

for x being set st f | A = g | A holds

(F [:] (f,x)) | A = (F [:] (g,x)) | A

for A being set

for F being Function

for x being set st f | A = g | A holds

(F [:] (f,x)) | A = (F [:] (g,x)) | A

proof end;

theorem Th37: :: FUNCOP_1:37

proof end;

theorem :: FUNCOP_1:38

canceled;

theorem :: FUNCOP_1:39

for f being Function

for A being set

for F being Function

for x being set holds (F [:] (f,x)) * (id A) = F [:] ((f | A),x)

for A being set

for F being Function

for x being set holds (F [:] (f,x)) * (id A) = F [:] ((f | A),x)

proof end;

definition

let F be Function;

let x be set ;

let g be Function;

func F [;] (x,g) -> set equals :: FUNCOP_1:def 5

F * <:((dom g) --> x),g:>;

correctness

coherence

F * <:((dom g) --> x),g:> is set ;

;

end;
let x be set ;

let g be Function;

func F [;] (x,g) -> set equals :: FUNCOP_1:def 5

F * <:((dom g) --> x),g:>;

correctness

coherence

F * <:((dom g) --> x),g:> is set ;

;

:: deftheorem defines [;] FUNCOP_1:def 5 :

for F being Function

for x being set

for g being Function holds F [;] (x,g) = F * <:((dom g) --> x),g:>;

registration

let F be Function;

let x be set ;

let g be Function;

cluster F [;] (x,g) -> Relation-like Function-like ;

coherence

( F [;] (x,g) is Function-like & F [;] (x,g) is Relation-like ) ;

end;
let x be set ;

let g be Function;

cluster F [;] (x,g) -> Relation-like Function-like ;

coherence

( F [;] (x,g) is Function-like & F [;] (x,g) is Relation-like ) ;

theorem :: FUNCOP_1:40

canceled;

theorem :: FUNCOP_1:41

theorem Th42: :: FUNCOP_1:42

for f, F being Function

for x, z being set st x in dom (F [;] (z,f)) holds

(F [;] (z,f)) . x = F . (z,(f . x))

for x, z being set st x in dom (F [;] (z,f)) holds

(F [;] (z,f)) . x = F . (z,(f . x))

proof end;

theorem :: FUNCOP_1:43

for f, g being Function

for A being set

for F being Function

for x being set st f | A = g | A holds

(F [;] (x,f)) | A = (F [;] (x,g)) | A

for A being set

for F being Function

for x being set st f | A = g | A holds

(F [;] (x,f)) | A = (F [;] (x,g)) | A

proof end;

theorem Th44: :: FUNCOP_1:44

proof end;

theorem :: FUNCOP_1:45

canceled;

theorem :: FUNCOP_1:46

for f being Function

for A being set

for F being Function

for x being set holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A))

for A being set

for F being Function

for x being set holds (F [;] (x,f)) * (id A) = F [;] (x,(f | A))

proof end;

theorem Th47: :: FUNCOP_1:47

for X being non empty set

for Y being set

for F being BinOp of X

for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X

for Y being set

for F being BinOp of X

for f, g being Function of Y,X holds F .: (f,g) is Function of Y,X

proof end;

definition

let X be non empty set ;

let Z be set ;

let F be BinOp of X;

let f, g be Function of Z,X;

:: original: .:

redefine func F .: (f,g) -> Function of Z,X;

coherence

F .: (f,g) is Function of Z,X by Th47;

end;
let Z be set ;

let F be BinOp of X;

let f, g be Function of Z,X;

:: original: .:

redefine func F .: (f,g) -> Function of Z,X;

coherence

F .: (f,g) is Function of Z,X by Th47;

theorem Th48: :: FUNCOP_1:48

for X, Y being non empty set

for F being BinOp of X

for f, g being Function of Y,X

for z being Element of Y holds (F .: (f,g)) . z = F . ((f . z),(g . z))

for F being BinOp of X

for f, g being Function of Y,X

for z being Element of Y holds (F .: (f,g)) . z = F . ((f . z),(g . z))

proof end;

theorem Th49: :: FUNCOP_1:49

for X, Y being non empty set

for F being BinOp of X

for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

for F being BinOp of X

for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

proof end;

theorem :: FUNCOP_1:50

canceled;

theorem :: FUNCOP_1:51

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f))

for F being BinOp of X

for f being Function of Y,X

for g being Function of X,X holds (F .: ((id X),g)) * f = F .: (f,(g * f))

proof end;

theorem :: FUNCOP_1:52

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

for F being BinOp of X

for f being Function of Y,X

for g being Function of X,X holds (F .: (g,(id X))) * f = F .: ((g * f),f)

proof end;

theorem :: FUNCOP_1:53

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X holds (F .: ((id X),(id X))) * f = F .: (f,f)

for F being BinOp of X

for f being Function of Y,X holds (F .: ((id X),(id X))) * f = F .: (f,f)

proof end;

theorem :: FUNCOP_1:54

for X being non empty set

for F being BinOp of X

for x being Element of X

for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x))

for F being BinOp of X

for x being Element of X

for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x))

proof end;

theorem :: FUNCOP_1:55

for X being non empty set

for F being BinOp of X

for x being Element of X

for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x)

for F being BinOp of X

for x being Element of X

for g being Function of X,X holds (F .: (g,(id X))) . x = F . ((g . x),x)

proof end;

theorem :: FUNCOP_1:56

for X being non empty set

for F being BinOp of X

for x being Element of X holds (F .: ((id X),(id X))) . x = F . (x,x)

for F being BinOp of X

for x being Element of X holds (F .: ((id X),(id X))) . x = F . (x,x)

proof end;

theorem Th57: :: FUNCOP_1:57

proof end;

definition

let I, i be set ;

:: original: -->

redefine func I --> i -> Function of I,{i};

coherence

I --> i is Function of I,{i}

end;
:: original: -->

redefine func I --> i -> Function of I,{i};

coherence

I --> i is Function of I,{i}

proof end;

definition

let B be non empty set ;

let A be set ;

let b be Element of B;

:: original: -->

redefine func A --> b -> Function of A,B;

coherence

A --> b is Function of A,B by Th57;

end;
let A be set ;

let b be Element of B;

:: original: -->

redefine func A --> b -> Function of A,B;

coherence

A --> b is Function of A,B by Th57;

theorem :: FUNCOP_1:58

for A being set

for X being non empty set

for x being Element of X holds A --> x is Function of A,X ;

for X being non empty set

for x being Element of X holds A --> x is Function of A,X ;

theorem Th59: :: FUNCOP_1:59

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X holds F [:] (f,x) is Function of Y,X

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X holds F [:] (f,x) is Function of Y,X

proof end;

definition

let X be non empty set ;

let Z be set ;

let F be BinOp of X;

let f be Function of Z,X;

let x be Element of X;

:: original: [:]

redefine func F [:] (f,x) -> Function of Z,X;

coherence

F [:] (f,x) is Function of Z,X by Th59;

end;
let Z be set ;

let F be BinOp of X;

let f be Function of Z,X;

let x be Element of X;

:: original: [:]

redefine func F [:] (f,x) -> Function of Z,X;

coherence

F [:] (f,x) is Function of Z,X by Th59;

theorem Th60: :: FUNCOP_1:60

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X

for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x)

for F being BinOp of X

for f being Function of Y,X

for x being Element of X

for y being Element of Y holds (F [:] (f,x)) . y = F . ((f . y),x)

proof end;

theorem Th61: :: FUNCOP_1:61

for X, Y being non empty set

for F being BinOp of X

for g, f being Function of Y,X

for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds

g = F [:] (f,x)

for F being BinOp of X

for g, f being Function of Y,X

for x being Element of X st ( for y being Element of Y holds g . y = F . ((f . y),x) ) holds

g = F [:] (f,x)

proof end;

theorem :: FUNCOP_1:62

canceled;

theorem :: FUNCOP_1:63

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x)

for F being BinOp of X

for f being Function of Y,X

for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x)

proof end;

theorem :: FUNCOP_1:64

for X being non empty set

for F being BinOp of X

for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x)

for F being BinOp of X

for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x)

proof end;

theorem Th65: :: FUNCOP_1:65

for X being non empty set

for Y being set

for F being BinOp of X

for g being Function of Y,X

for x being Element of X holds F [;] (x,g) is Function of Y,X

for Y being set

for F being BinOp of X

for g being Function of Y,X

for x being Element of X holds F [;] (x,g) is Function of Y,X

proof end;

definition

let X be non empty set ;

let Z be set ;

let F be BinOp of X;

let x be Element of X;

let g be Function of Z,X;

:: original: [;]

redefine func F [;] (x,g) -> Function of Z,X;

coherence

F [;] (x,g) is Function of Z,X by Th65;

end;
let Z be set ;

let F be BinOp of X;

let x be Element of X;

let g be Function of Z,X;

:: original: [;]

redefine func F [;] (x,g) -> Function of Z,X;

coherence

F [;] (x,g) is Function of Z,X by Th65;

theorem Th66: :: FUNCOP_1:66

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X

for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y))

for F being BinOp of X

for f being Function of Y,X

for x being Element of X

for y being Element of Y holds (F [;] (x,f)) . y = F . (x,(f . y))

proof end;

theorem Th67: :: FUNCOP_1:67

for X, Y being non empty set

for F being BinOp of X

for g, f being Function of Y,X

for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds

g = F [;] (x,f)

for F being BinOp of X

for g, f being Function of Y,X

for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds

g = F [;] (x,f)

proof end;

theorem :: FUNCOP_1:68

canceled;

theorem :: FUNCOP_1:69

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f)

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X holds (F [;] (x,(id X))) * f = F [;] (x,f)

proof end;

theorem :: FUNCOP_1:70

for X being non empty set

for F being BinOp of X

for x being Element of X holds (F [;] (x,(id X))) . x = F . (x,x)

for F being BinOp of X

for x being Element of X holds (F [;] (x,(id X))) . x = F . (x,x)

proof end;

theorem :: FUNCOP_1:71

for X, Y, Z being non empty set

for f being Function of X,[:Y,Z:]

for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]

for f being Function of X,[:Y,Z:]

for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]

proof end;

definition

let X, Y, Z be non empty set ;

let f be Function of X,[:Y,Z:];

:: original: proj2

redefine func rng f -> Relation of Y,Z;

coherence

proj2 f is Relation of Y,Z by RELAT_1:def 19;

end;
let f be Function of X,[:Y,Z:];

:: original: proj2

redefine func rng f -> Relation of Y,Z;

coherence

proj2 f is Relation of Y,Z by RELAT_1:def 19;

definition

let X, Y, Z be non empty set ;

let f be Function of X,[:Y,Z:];

:: original: ~

redefine func f ~ -> Function of X,[:Z,Y:];

coherence

f ~ is Function of X,[:Z,Y:]

end;
let f be Function of X,[:Y,Z:];

:: original: ~

redefine func f ~ -> Function of X,[:Z,Y:];

coherence

f ~ is Function of X,[:Z,Y:]

proof end;

theorem :: FUNCOP_1:72

canceled;

theorem :: FUNCOP_1:73

proof end;

theorem :: FUNCOP_1:74

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x1, x2 being Element of X st F is associative holds

F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x1, x2 being Element of X st F is associative holds

F [:] ((F [;] (x1,f)),x2) = F [;] (x1,(F [:] (f,x2)))

proof end;

theorem :: FUNCOP_1:75

for X being non empty set

for Y being set

for F being BinOp of X

for f, g being Function of Y,X

for x being Element of X st F is associative holds

F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))

for Y being set

for F being BinOp of X

for f, g being Function of Y,X

for x being Element of X st F is associative holds

F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))

proof end;

theorem :: FUNCOP_1:76

for X being non empty set

for Y being set

for F being BinOp of X

for f, g, h being Function of Y,X st F is associative holds

F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h)))

for Y being set

for F being BinOp of X

for f, g, h being Function of Y,X st F is associative holds

F .: ((F .: (f,g)),h) = F .: (f,(F .: (g,h)))

proof end;

theorem :: FUNCOP_1:77

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x1, x2 being Element of X st F is associative holds

F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x1, x2 being Element of X st F is associative holds

F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))

proof end;

theorem :: FUNCOP_1:78

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x1, x2 being Element of X st F is associative holds

F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2)

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x1, x2 being Element of X st F is associative holds

F [:] (f,(F . (x1,x2))) = F [:] ((F [:] (f,x1)),x2)

proof end;

theorem :: FUNCOP_1:79

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

for Y being set

for F being BinOp of X

for f being Function of Y,X

for x being Element of X st F is commutative holds

F [;] (x,f) = F [:] (f,x)

proof end;

theorem :: FUNCOP_1:80

for X being non empty set

for Y being set

for F being BinOp of X

for f, g being Function of Y,X st F is commutative holds

F .: (f,g) = F .: (g,f)

for Y being set

for F being BinOp of X

for f, g being Function of Y,X st F is commutative holds

F .: (f,g) = F .: (g,f)

proof end;

theorem :: FUNCOP_1:81

for X being non empty set

for Y being set

for F being BinOp of X

for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

for Y being set

for F being BinOp of X

for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

proof end;

theorem :: FUNCOP_1:82

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for y being Element of Y st F is idempotent holds

(F [;] ((f . y),f)) . y = f . y

for F being BinOp of X

for f being Function of Y,X

for y being Element of Y st F is idempotent holds

(F [;] ((f . y),f)) . y = f . y

proof end;

theorem :: FUNCOP_1:83

for X, Y being non empty set

for F being BinOp of X

for f being Function of Y,X

for y being Element of Y st F is idempotent holds

(F [:] (f,(f . y))) . y = f . y

for F being BinOp of X

for f being Function of Y,X

for y being Element of Y st F is idempotent holds

(F [:] (f,(f . y))) . y = f . y

proof end;

theorem :: FUNCOP_1:84

for F, f, g being Function st [:(rng f),(rng g):] c= dom F holds

dom (F .: (f,g)) = (dom f) /\ (dom g)

dom (F .: (f,g)) = (dom f) /\ (dom g)

proof end;

definition

let IT be Function;

attr IT is Function-yielding means :Def6: :: FUNCOP_1:def 6

for x being set st x in dom IT holds

IT . x is Function;

end;
attr IT is Function-yielding means :Def6: :: FUNCOP_1:def 6

for x being set st x in dom IT holds

IT . x is Function;

:: deftheorem Def6 defines Function-yielding FUNCOP_1:def 6 :

for IT being Function holds

( IT is Function-yielding iff for x being set st x in dom IT holds

IT . x is Function );

registration

cluster Relation-like Function-like Function-yielding set ;

existence

ex b_{1} being Function st b_{1} is Function-yielding

end;
existence

ex b

proof end;

registration

let B be Function-yielding Function;

let j be set ;

cluster B . j -> Relation-like Function-like ;

coherence

( B . j is Function-like & B . j is Relation-like )

end;
let j be set ;

cluster B . j -> Relation-like Function-like ;

coherence

( B . j is Function-like & B . j is Relation-like )

proof end;

registration

let F be Function-yielding Function;

let f be Function;

cluster f * F -> Function-yielding ;

coherence

F * f is Function-yielding

end;
let f be Function;

cluster f * F -> Function-yielding ;

coherence

F * f is Function-yielding

proof end;

registration

let B be set ;

let c be non empty set ;

cluster B --> c -> non-empty ;

coherence

B --> c is non-empty

end;
let c be non empty set ;

cluster B --> c -> non-empty ;

coherence

B --> c is non-empty

proof end;

theorem :: FUNCOP_1:85

for z being set

for X, Y being non empty set

for x being Element of X

for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z

for X, Y being non empty set

for x being Element of X

for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z

proof end;

definition

let a, b, c be set ;

func (a,b) .--> c -> Function equals :: FUNCOP_1:def 7

{[a,b]} --> c;

coherence

{[a,b]} --> c is Function ;

end;
func (a,b) .--> c -> Function equals :: FUNCOP_1:def 7

{[a,b]} --> c;

coherence

{[a,b]} --> c is Function ;

:: deftheorem defines .--> FUNCOP_1:def 7 :

for a, b, c being set holds (a,b) .--> c = {[a,b]} --> c;

theorem :: FUNCOP_1:86

proof end;

definition

let x, y, a, b be set ;

func IFEQ (x,y,a,b) -> set equals :Def8: :: FUNCOP_1:def 8

a if x = y

otherwise b;

correctness

coherence

( ( x = y implies a is set ) & ( not x = y implies b is set ) );

consistency

for b_{1} being set holds verum;

;

end;
func IFEQ (x,y,a,b) -> set equals :Def8: :: FUNCOP_1:def 8

a if x = y

otherwise b;

correctness

coherence

( ( x = y implies a is set ) & ( not x = y implies b is set ) );

consistency

for b

;

:: deftheorem Def8 defines IFEQ FUNCOP_1:def 8 :

for x, y, a, b being set holds

( ( x = y implies IFEQ (x,y,a,b) = a ) & ( not x = y implies IFEQ (x,y,a,b) = b ) );

definition

let D be set ;

let x, y be set ;

let a, b be Element of D;

:: original: IFEQ

redefine func IFEQ (x,y,a,b) -> Element of D;

coherence

IFEQ (x,y,a,b) is Element of D

end;
let x, y be set ;

let a, b be Element of D;

:: original: IFEQ

redefine func IFEQ (x,y,a,b) -> Element of D;

coherence

IFEQ (x,y,a,b) is Element of D

proof end;

definition

let x, y be set ;

func x .--> y -> set equals :: FUNCOP_1:def 9

{x} --> y;

coherence

{x} --> y is set ;

end;
func x .--> y -> set equals :: FUNCOP_1:def 9

{x} --> y;

coherence

{x} --> y is set ;

:: deftheorem defines .--> FUNCOP_1:def 9 :

for x, y being set holds x .--> y = {x} --> y;

registration

let x, y be set ;

cluster x .--> y -> Relation-like Function-like ;

coherence

( x .--> y is Function-like & x .--> y is Relation-like ) ;

end;
cluster x .--> y -> Relation-like Function-like ;

coherence

( x .--> y is Function-like & x .--> y is Relation-like ) ;

registration
end;

theorem Th87: :: FUNCOP_1:87

proof end;

theorem :: FUNCOP_1:88

proof end;

Lm2: for o, m, r being set holds (o,m) :-> r is Function of [:{o},{m}:],{r}

proof end;

definition

let o, m, r be set ;

:: original: .-->

redefine func (o,m) :-> r -> Function of [:{o},{m}:],{r} means :: FUNCOP_1:def 10

verum;

coherence

(o,m) .--> r is Function of [:{o},{m}:],{r} by Lm2;

compatibility

for b_{1} being Function of [:{o},{m}:],{r} holds

( b_{1} = (o,m) .--> r iff verum )

end;
:: original: .-->

redefine func (o,m) :-> r -> Function of [:{o},{m}:],{r} means :: FUNCOP_1:def 10

verum;

coherence

(o,m) .--> r is Function of [:{o},{m}:],{r} by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines :-> FUNCOP_1:def 10 :

for o, m, r being set

for b

( b

theorem :: FUNCOP_1:89

proof end;

theorem :: FUNCOP_1:90

proof end;

theorem :: FUNCOP_1:91

proof end;

definition

let m, o be set ;

:: original: .-->

redefine func m :-> o -> Function of {m},{o};

coherence

m .--> o is Function of {m},{o} ;

end;
:: original: .-->

redefine func m :-> o -> Function of {m},{o};

coherence

m .--> o is Function of {m},{o} ;

theorem :: FUNCOP_1:92

for a, b, c being set

for x being Element of {a}

for y being Element of {b} holds ((a,b) :-> c) . (x,y) = c by TARSKI:def 1;

for x being Element of {a}

for y being Element of {b} holds ((a,b) :-> c) . (x,y) = c by TARSKI:def 1;

registration

let f be Function-yielding Function;

let C be set ;

cluster f | C -> Function-yielding ;

coherence

f | C is Function-yielding

end;
let C be set ;

cluster f | C -> Function-yielding ;

coherence

f | C is Function-yielding

proof end;

registration

let A be set ;

let f be Function;

cluster A --> f -> Function-yielding ;

coherence

A --> f is Function-yielding

end;
let f be Function;

cluster A --> f -> Function-yielding ;

coherence

A --> f is Function-yielding

proof end;

registration
end;

registration

cluster Relation-like Function-like constant non empty set ;

existence

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is constant )

end;
existence

ex b

( not b

proof end;

registration

let f be constant Function;

let X be set ;

cluster f | X -> constant ;

coherence

f | X is constant

end;
let X be set ;

cluster f | X -> constant ;

coherence

f | X is constant

proof end;

theorem :: FUNCOP_1:93

for f being constant non empty Function ex y being set st

for x being set st x in dom f holds

f . x = y

for x being set st x in dom f holds

f . x = y

proof end;

theorem :: FUNCOP_1:94

proof end;

theorem :: FUNCOP_1:95

proof end;

registration

let X be set ;

let Y be non empty set ;

cluster Relation-like X -defined Y -valued Function-like total Element of bool [:X,Y:];

existence

ex b_{1} being PartFunc of X,Y st b_{1} is total

end;
let Y be non empty set ;

cluster Relation-like X -defined Y -valued Function-like total Element of bool [:X,Y:];

existence

ex b

proof end;

registration
end;

registration
end;

theorem :: FUNCOP_1:96

registration

let I be set ;

let f be Function;

cluster I .--> f -> Function-yielding ;

coherence

I .--> f is Function-yielding ;

end;
let f be Function;

cluster I .--> f -> Function-yielding ;

coherence

I .--> f is Function-yielding ;

registration

let I be set ;

cluster Relation-like non-empty I -defined Function-like total set ;

existence

ex b_{1} being non-empty I -defined Function st b_{1} is total

end;
cluster Relation-like non-empty I -defined Function-like total set ;

existence

ex b

proof end;

theorem Th97: :: FUNCOP_1:97

proof end;

theorem :: FUNCOP_1:98

proof end;

registration

let I, A be set ;

cluster I --> A -> I -defined total I -defined Function;

coherence

for b_{1} being I -defined Function st b_{1} = I --> A holds

b_{1} is total
;

end;
cluster I --> A -> I -defined total I -defined Function;

coherence

for b

b

theorem :: FUNCOP_1:99

proof end;

registration

let A be non empty set ;

let x be set ;

let i be Element of A;

cluster x .--> i -> A -valued ;

coherence

x .--> i is A -valued

end;
let x be set ;

let i be Element of A;

cluster x .--> i -> A -valued ;

coherence

x .--> i is A -valued

proof end;

theorem :: FUNCOP_1:100

for X being non empty set

for F being BinOp of X

for Y being set

for f, g being Function of Y,X

for x being Element of X st F is associative holds

F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g)))

for F being BinOp of X

for Y being set

for f, g being Function of Y,X

for x being Element of X st F is associative holds

F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g)))

proof end;

registration

let A be set ;

let B be non empty set ;

let x be Element of B;

cluster A --> x -> B -valued ;

coherence

A --> x is B -valued ;

end;
let B be non empty set ;

let x be Element of B;

cluster A --> x -> B -valued ;

coherence

A --> x is B -valued ;

registration

let A be non empty set ;

let x be Element of A;

let y be set ;

cluster x .--> y -> A -defined ;

coherence

x .--> y is A -defined

end;
let x be Element of A;

let y be set ;

cluster x .--> y -> A -defined ;

coherence

x .--> y is A -defined

proof end;