:: by Andrzej Trybulec

::

:: Received September 4, 1989

:: Copyright (c) 1990-2018 Association of Mizar Users

definition

let f be Function;

ex b_{1} being Function st

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

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

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

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

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

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

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

b_{2} . x = [z,y] ) & ( f . x = b_{2} . x or ex y, z being object 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 object st x in dom b_{2} holds

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

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

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

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

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

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

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

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

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

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

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

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

ex b

( dom b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

involutiveness for b

( ( for y, z being object st b

b

( dom b

( ( for y, z being object st b

b

proof end;

:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :

for f, b_{2} being Function holds

( b_{2} = f ~ iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

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

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

for f, b

( b

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

b

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

for A being set

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

for A being set

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

registration

let A be set ;

let z be object ;

coherence

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

end;
let z be object ;

coherence

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

proof end;

theorem :: FUNCOP_1:8

registration
end;

registration
end;

theorem Th11: :: FUNCOP_1:11

for f being Function

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

f . z = x ) holds

f = (dom f) --> x

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

f . z = x ) holds

f = (dom f) --> x

proof end;

theorem :: FUNCOP_1:17

for h being Function

for A being set

for x being object st x in dom h holds

h * (A --> x) = A --> (h . x)

for A being set

for x being object st x in dom h holds

h * (A --> x) = A --> (h . x)

proof end;

theorem :: FUNCOP_1:18

for h being Function

for A being set

for x being object st A <> {} & x in dom h holds

dom (h * (A --> x)) <> {}

for A being set

for x being object st A <> {} & x in dom h holds

dom (h * (A --> x)) <> {}

proof end;

:: deftheorem defines .: FUNCOP_1:def 3 :

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

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

registration
end;

Lm1: for f, g, F being Function

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

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

proof end;

theorem :: FUNCOP_1:21

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

theorem Th23: :: FUNCOP_1:23

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 Th24: :: FUNCOP_1:24

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;

definition
end;

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

for F, f being Function

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

for F, f being Function

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

registration

let F, f be Function;

let x be object ;

coherence

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

end;
let x be object ;

coherence

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

theorem :: FUNCOP_1:26

theorem Th27: :: FUNCOP_1:27

for f, F being Function

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

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

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

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

proof end;

theorem :: FUNCOP_1:28

for f, g being Function

for A being set

for F being Function

for x being object 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 object st f | A = g | A holds

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

proof end;

theorem :: FUNCOP_1:30

for f being Function

for A being set

for F being Function

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

for A being set

for F being Function

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

proof end;

definition

let F be Function;

let x be object ;

let g be Function;

correctness

coherence

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

;

end;
let x be object ;

let g be Function;

correctness

coherence

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

;

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

for F being Function

for x being object

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

for F being Function

for x being object

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

registration

let F be Function;

let x be object ;

let g be Function;

coherence

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

end;
let x be object ;

let g be Function;

coherence

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

theorem :: FUNCOP_1:31

theorem Th32: :: FUNCOP_1:32

for f, F being Function

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

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

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

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

proof end;

theorem :: FUNCOP_1:33

for f, g being Function

for A being set

for F being Function

for x being object 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 object st f | A = g | A holds

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

proof end;

theorem :: FUNCOP_1:35

for f being Function

for A being set

for F being Function

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

for A being set

for F being Function

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

proof end;

theorem Th36: :: FUNCOP_1:36

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

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

theorem Th37: :: FUNCOP_1:37

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 Th38: :: FUNCOP_1:38

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

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

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

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

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

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

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 Th45: :: FUNCOP_1:45

for A, B being set

for X being non empty set

for x being Element of X st x in B holds

A --> x is Function of A,B

for X being non empty set

for x being Element of X st x in B holds

A --> x is Function of A,B

proof end;

definition

let I be set ;

let i be object ;

:: original: -->

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

coherence

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

end;
let i be object ;

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

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

theorem :: FUNCOP_1:46

theorem Th47: :: FUNCOP_1:47

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

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

theorem Th48: :: FUNCOP_1:48

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 Th49: :: FUNCOP_1:49

for X, Y being non empty set

for F being BinOp of X

for f, g 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 f, g 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:50

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

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 Th52: :: FUNCOP_1:52

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

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

theorem Th53: :: FUNCOP_1:53

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 Th54: :: FUNCOP_1:54

for X, Y being non empty set

for F being BinOp of X

for f, g 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 f, g 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:55

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

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

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

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

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

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

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

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

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

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

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

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;

:: Addendum, 2002.07.08

theorem :: FUNCOP_1:69

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;

:: from PRALG_1, 2004.07.23

definition

let IT be Function;

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

for x being object st x in dom IT holds

IT . x is Function;

for x being object 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 object st x in dom IT holds

IT . x is Function );

for IT being Function holds

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

IT . x is Function );

registration

let B be Function-yielding Function;

let j be object ;

coherence

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

end;
let j be object ;

coherence

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

proof end;

registration

let F be Function-yielding Function;

let f be Function;

coherence

F * f is Function-yielding

end;
let f be Function;

coherence

F * f is Function-yielding

proof end;

:: missing, 2005.11.13, A.T.

:: missing, 2005.12.20, A.T.

theorem :: FUNCOP_1:70

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

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

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

:: from CQC_LANG, 2007.03.13, A.T.

definition

let x, y, a, b be object ;

correctness

coherence

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

consistency

for b_{1} being object holds verum;

;

end;
correctness

coherence

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

consistency

for b

;

:: deftheorem Def8 defines IFEQ FUNCOP_1:def 8 :

for x, y, a, b being object holds

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

for x, y, a, b being object holds

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

definition

let x, y be object ;

let a, b be set ;

:: original: IFEQ

redefine func IFEQ (x,y,a,b) -> set ;

correctness

coherence

IFEQ (x,y,a,b) is set ;

end;
let a, b be set ;

:: original: IFEQ

redefine func IFEQ (x,y,a,b) -> set ;

correctness

coherence

IFEQ (x,y,a,b) is set ;

proof end;

definition

let D be set ;

let x, y be object ;

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

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;

registration
end;

registration
end;

:: from SCMFSA6A, 2007.07.22, A.T.

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

proof end;

definition

let o, m, r be object ;

(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 redefine func (o,m) :-> r -> Function of [:{o},{m}:],{r} means :: FUNCOP_1:def 10

verum;

(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 object

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

( b_{4} = (o,m) :-> r iff verum );

for o, m, r being object

for b

( b

:: missing, 2008.04.15, A.T.

definition

let m, o be object ;

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

:: from MSUHOM_1, ALTCAT_1, 2008.07.06, A.T.

registration
end;

:: from CIRCCOMB, 2008.07.06, A.T.

:: from SEQM_3, 2008.07.17, A.T.

:: from YELLOW_6, 2008.07.17, A.T.

registration

existence

ex b_{1} being Function st

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

let Y be non empty set ;

ex b_{1} being Function of X,Y st b_{1} is constant

end;
ex b

( not b

proof end;

let X be set ;let Y be non empty set ;

cluster Relation-like X -defined Y -valued Function-like constant total quasi_total for Function of ,;

existence ex b

proof end;

:: missing, 2008.07.17, A.T.

:: missing, 2008.08.14, A.T.

theorem :: FUNCOP_1:78

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

for x being object st x in dom f holds

f . x = y

for x being object st x in dom f holds

f . x = y

proof end;

:: from YELLOW_6, 2008.12.26, A.T.

:: from CIRCCMB3, 2008.12.26, A.T.

:: missing, 2009.01.21, A.T.

registration

let X be set ;

let Y be non empty set ;

existence

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

end;
let Y be non empty set ;

existence

ex b

proof end;

:: new, 2009.02.14, A.T.

registration
end;

registration
end;

:: BORSUK_1:6, 2009.06.11, A.K.

:: 2009.10.03, A.T.

registration
end;

registration

let I be set ;

let A be object ;

coherence

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

b_{1} is total
;

end;
let A be object ;

coherence

for b

b

registration

let A be non empty set ;

let x be set ;

let i be Element of A;

coherence

x .--> i is A -valued

end;
let x be set ;

let i be Element of A;

coherence

x .--> i is A -valued

proof end;

:: missing, 2010.02.10, A.T.

theorem :: FUNCOP_1:85

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

registration

let A be non empty set ;

let x be Element of A;

let y be object ;

coherence

x .--> y is A -defined

end;
let x be Element of A;

let y be object ;

coherence

x .--> y is A -defined

proof end;

:: missing, 2011.02.06, A.K.

registration

let Y be functional set ;

coherence

for b_{1} being Function st b_{1} is Y -valued holds

b_{1} is Function-yielding
;

end;
coherence

for b

b

:: from MSUALG_4, 2011.04.16, A.T.

definition

let IT be Function;

end;
attr IT is Relation-yielding means :: FUNCOP_1:def 11

for x being set st x in dom IT holds

IT . x is Relation;

for x being set st x in dom IT holds

IT . x is Relation;

:: deftheorem defines Relation-yielding FUNCOP_1:def 11 :

for IT being Function holds

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

IT . x is Relation );

for IT being Function holds

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

IT . x is Relation );

registration
end;

registration
end;

:: from CIRCCOMB, 2011.04.19, A.T.

theorem :: FUNCOP_1:87

for X, Y being set

for x, y being object holds

( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )

for x, y being object holds

( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )

proof end;

registration

let f be Function-yielding Function;

let a, b be object ;

coherence

( f . (a,b) is Function-like & f . (a,b) is Relation-like ) ;

end;
let a, b be object ;

coherence

( f . (a,b) is Function-like & f . (a,b) is Relation-like ) ;

registration

let Y be set ;

let X, Z be non empty set ;

coherence

for b_{1} being Function of X,(Funcs (Y,Z)) holds b_{1} is Function-yielding
;

end;
let X, Z be non empty set ;

coherence

for b