:: Binary Operations Applied to Functions
:: by Andrzej Trybulec
::
:: Received September 4, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: FUNCOP_1:1

for A being set holds delta A = <:(id A),(id A):>

proof end;

definition

let f be Function;

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
ex b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b₁ . x = [z,y] ) & ( f . x = b₁ . x or ex y, z being object st f . x = [y,z] ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b₁ . x = [z,y] ) & ( f . x = b₁ . x or ex y, z being object st f . x = [y,z] ) ) ) & dom b₂ = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b₂ . x = [z,y] ) & ( f . x = b₂ . x or ex y, z being object st f . x = [y,z] ) ) ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Function st dom b₁ = dom b₂ & ( for x being object st x in dom b₂ holds
( ( for y, z being object st b₂ . x = [y,z] holds
b₁ . x = [z,y] ) & ( b₂ . x = b₁ . x or ex y, z being object st b₂ . x = [y,z] ) ) ) holds
( dom b₂ = dom b₁ & ( for x being object st x in dom b₁ holds
( ( for y, z being object st b₁ . x = [y,z] holds
b₂ . x = [z,y] ) & ( b₁ . x = b₂ . x or ex y, z being object st b₁ . x = [y,z] ) ) ) )

proof end;

end;

:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :
for f, b₂ being Function holds
( b₂ = f ~ iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b₂ . x = [z,y] ) & ( f . x = b₂ . x or ex y, z being object st f . x = [y,z] ) ) ) ) );

theorem Th2: :: FUNCOP_1:2

for f, g being Function holds <:f,g:> = <:g,f:> ~

proof end;

theorem Th3: :: FUNCOP_1:3

for f being Function
for A being set holds (f | A) ~ = (f ~) | A

proof end;

theorem :: FUNCOP_1:4

for A being set holds (delta A) ~ = delta A

proof end;

theorem Th5: :: FUNCOP_1:5

for f, g being Function
for A being set holds <:f,g:> | A = <:(f | A),g:>

proof end;

theorem Th6: :: FUNCOP_1:6

for f, g being Function
for A being set holds <:f,g:> | A = <:f,(g | A):>

proof end;

definition

let A be set ;
let z be object ;

func A --> z -> set equals :: FUNCOP_1:def 2
[:A,{z}:];

coherence
[:A,{z}:] is set ;

end;

:: deftheorem defines --> FUNCOP_1:def 2 :
for A being set
for z being object holds A --> z = [:A,{z}:];

registration

let A be set ;
let z be object ;

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

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

proof end;

end;

theorem Th7: :: FUNCOP_1:7

for A being set
for x, z being object st x in A holds
(A --> z) . x = z

proof end;

registration

let A be non empty set ;
let x be object ;
let a be Element of A;

reduce (A --> x) . a to x;

reducibility
(A --> x) . a = x by Th7;

end;

theorem :: FUNCOP_1:8

for A being set
for x being object st A <> {} holds
rng (A --> x) = {x} by RELAT_1:160;

theorem Th9: :: FUNCOP_1:9

for f being Function
for x being object st rng f = {x} holds
f = (dom f) --> x

proof end;

registration

let x be object ;

cluster {} --> x -> empty ;

coherence
{} --> x is empty by ZFMISC_1:90;

end;

registration

let x be object ;
let A be empty set ;

cluster A --> x -> empty ;

coherence
A --> x is empty ;

end;

registration

let x be object ;
let A be non empty set ;

cluster A --> x -> non empty ;

coherence
not A --> x is empty ;

end;

theorem :: FUNCOP_1:10

for x being object holds
( dom ({} --> x) = {} & rng ({} --> x) = {} ) ;

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

proof end;

theorem Th12: :: FUNCOP_1:12

for A, B being set
for x being object holds (A --> x) | B = (A /\ B) --> x

proof end;

theorem Th13: :: FUNCOP_1:13

for A being set
for x being object holds
( dom (A --> x) = A & rng (A --> x) c= {x} )

proof end;

registration

let X be set ;
let a be object ;

reduce dom (X --> a) to X;

reducibility
dom (X --> a) = X by Th13;

end;

registration

let D be set ;

cluster D --> {} -> empty-yielding ;

coherence
D --> {} is empty-yielding by Th13;

end;

theorem Th14: :: FUNCOP_1:14

for A, B being set
for x being object st x in B holds
(A --> x) " B = A

proof end;

theorem :: FUNCOP_1:15

for A being set
for x being object holds (A --> x) " {x} = A

proof end;

theorem :: FUNCOP_1:16

for A, B being set
for x being object st not x in B holds
(A --> x) " B = {}

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)

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

proof end;

theorem :: FUNCOP_1:19

for h being Function
for A being set
for x being object holds (A --> x) * h = (h " A) --> x

proof end;

theorem :: FUNCOP_1:20

for A, y being set
for x being object holds (A --> [x,y]) ~ = A --> [y,x]

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;

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

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)

proof end;

theorem :: FUNCOP_1:22

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)) by Lm1;

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

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

proof end;

theorem Th25: :: FUNCOP_1:25

for f, g, h, F being Function holds (F .: (f,g)) * h = F .: ((f * h),(g * h))

proof end;

definition

let F, f be Function;
let x be object ;

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;

:: deftheorem defines [:] FUNCOP_1:def 4 :
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 ;

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

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

end;

theorem :: FUNCOP_1:26

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

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)

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

proof end;

theorem Th29: :: FUNCOP_1:29

for f, h, F being Function
for x being object holds (F [:] (f,x)) * h = F [:] ((f * h),x)

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)

proof end;

definition

let F be Function;
let x be object ;
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;

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

registration

let F be Function;
let x be object ;
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;

theorem :: FUNCOP_1:31

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

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

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

proof end;

theorem Th34: :: FUNCOP_1:34

for f, h, F being Function
for x being object holds (F [;] (x,f)) * h = F [;] (x,(f * h))

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

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

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;

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

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)

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

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)

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)

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

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)

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)

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

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}

proof end;

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;

theorem :: FUNCOP_1:46

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

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

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;

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)

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)

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)

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)

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

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;

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

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)

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)

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)

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

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;

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

proof end;

end;

theorem :: FUNCOP_1:58

for X, Y, Z being non empty set
for f being Function of X,[:Y,Z:] holds rng (f ~) = (rng f) ~

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

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

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

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

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)

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)

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)

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

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

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

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)

proof end;

:: from PRALG_1, 2004.07.23

definition

let IT be Function;

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;

end;

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

registration

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

existence
ex b₁ being Function st b₁ is Function-yielding

proof end;

end;

registration

let B be Function-yielding Function;
let j be object ;

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

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

proof end;

end;

registration

let F be Function-yielding Function;
let f be Function;

cluster f * F -> Function-yielding ;

coherence
F * f is Function-yielding

proof end;

end;

:: missing, 2005.11.13, A.T.

registration

let B be set ;
let c be non empty set ;

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

coherence
B --> c is non-empty

proof end;

end;

:: missing, 2005.12.20, A.T.

theorem :: FUNCOP_1:70

for z being object
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 by Th7, ZFMISC_1:87;

definition

let a, b, c be object ;

func (a,b) .--> c -> Function equals :: FUNCOP_1:def 7
{[a,b]} --> c;

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

end;

:: deftheorem defines .--> FUNCOP_1:def 7 :
for a, b, c being object holds (a,b) .--> c = {[a,b]} --> c;

theorem :: FUNCOP_1:71

for a, b, c being object holds ((a,b) .--> c) . (a,b) = c

proof end;

:: from CQC_LANG, 2007.03.13, A.T.

definition

let x, y, a, b be object ;

func IFEQ (x,y,a,b) -> object equals :Def8: :: FUNCOP_1:def 8
a if x = y
otherwise b;

correctness
coherence
( ( x = y implies a is object ) & ( not x = y implies b is object ) );
consistency
for b₁ being object holds verum;
;

end;

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

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 ;

proof end;

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

proof end;

end;

definition

let x, y be object ;

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

coherence
{x} --> y is set ;

end;

:: deftheorem defines .--> FUNCOP_1:def 9 :
for x, y being object holds x .--> y = {x} --> y;

registration

let x, y be object ;

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

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

end;

registration

let x, y be object ;

cluster x .--> y -> one-to-one ;

coherence
x .--> y is one-to-one

proof end;

end;

theorem Th72: :: FUNCOP_1:72

for x, y being object holds (x .--> y) . x = y

proof end;

:: from SCMFSA6A, 2007.07.22, A.T.

theorem :: FUNCOP_1:73

for a, b being object
for f being Function holds
( a .--> b c= f iff ( a in dom f & f . a = b ) )

proof end;

notation

let o, m, r be object ;
synonym (o,m) :-> r for (o,m) .--> r;

end;

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 ;

:: 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₁ being Function of [:{o},{m}:],{r} holds
( b₁ = (o,m) .--> r iff verum )

proof end;

end;

:: deftheorem defines :-> FUNCOP_1:def 10 :
for o, m, r being object
for b₄ being Function of [:{o},{m}:],{r} holds
( b₄ = (o,m) :-> r iff verum );

theorem :: FUNCOP_1:74

for x, y being object holds x in dom (x .--> y) by TARSKI:def 1;

theorem :: FUNCOP_1:75

for x, y, z being object st z in dom (x .--> y) holds
z = x by TARSKI:def 1;

:: missing, 2008.04.15, A.T.

theorem :: FUNCOP_1:76

for A being set
for x, y being object st not x in A holds
(x .--> y) | A = {}

proof end;

notation

let x, y be object ;
synonym x :-> y for x .--> y;

end;

definition

let m, o be object ;
:: original: .-->
redefine func m :-> o -> Function of {m},{o};
coherence
m .--> o is Function of {m},{o} ;

end;

theorem :: FUNCOP_1:77

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;

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

registration

let f be Function-yielding Function;
let C be set ;

cluster f | C -> Function-yielding ;

coherence
f | C is Function-yielding

proof end;

end;

:: from CIRCCOMB, 2008.07.06, A.T.

registration

let A be set ;
let f be Function;

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

coherence
A --> f is Function-yielding ;

end;

:: from SEQM_3, 2008.07.17, A.T.

registration

let X be set ;
let a be object ;

cluster X --> a -> constant ;

coherence
X --> a is constant

proof end;

end;

:: from YELLOW_6, 2008.07.17, A.T.

registration

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

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is constant )

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 Element of bool [:X,Y:];

existence
ex b₁ being Function of X,Y st b₁ is constant

proof end;

end;

:: missing, 2008.07.17, A.T.

registration

let f be constant Function;
let X be set ;

cluster f | X -> constant ;

coherence
f | X is constant

proof end;

end;

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

proof end;

:: from YELLOW_6, 2008.12.26, A.T.

theorem :: FUNCOP_1:79

for X being non empty set
for x being set holds the_value_of (X --> x) = x

proof end;

:: from CIRCCMB3, 2008.12.26, A.T.

theorem :: FUNCOP_1:80

for f being constant Function holds f = (dom f) --> (the_value_of f)

proof end;

:: missing, 2009.01.21, A.T.

registration

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

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

existence
ex b₁ being PartFunc of X,Y st b₁ is total

proof end;

end;

:: new, 2009.02.14, A.T.

registration

let I be set ;
let A be object ;

cluster I --> A -> I -defined ;

coherence
I --> A is I -defined ;

end;

registration

let I, A be object ;

cluster I .--> A -> {I} -defined ;

coherence
I .--> A is {I} -defined ;

end;

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

theorem :: FUNCOP_1:81

for A, B being set
for x being object holds (A --> x) .: B c= {x} ;

registration

let I be set ;
let f be Function;

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

coherence
I .--> f is Function-yielding ;

end;

:: 2009.10.03, A.T.

registration

let I be set ;

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

existence
ex b₁ being non-empty I -defined Function st b₁ is total

proof end;

end;

theorem Th82: :: FUNCOP_1:82

for x, y being object holds x .--> y is_isomorphism_of {[x,x]},{[y,y]}

proof end;

theorem :: FUNCOP_1:83

for x, y being object holds {[x,x]},{[y,y]} are_isomorphic

proof end;

registration

let I be set ;
let A be object ;

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

coherence
for b₁ being I -defined Function st b₁ = I --> A holds
b₁ is total ;

end;

theorem :: FUNCOP_1:84

for x being object
for f being Function st x in dom f holds
x .--> (f . x) c= f

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

proof end;

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

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;

registration

let A be non empty set ;
let x be Element of A;
let y be object ;

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

coherence
x .--> y is A -defined by ZFMISC_1:31;

end;

theorem :: FUNCOP_1:86

for x, y, A being set st x in A holds
(x .--> y) | A = x .--> y

proof end;

:: missing, 2011.02.06, A.K.

registration

let Y be functional set ;

cluster Relation-like Y -valued Function-like -> Function-yielding for set ;

coherence
for b₁ being Function st b₁ is Y -valued holds
b₁ is Function-yielding ;

end;

:: from MSUALG_4, 2011.04.16, A.T.

definition

let IT be Function;

attr IT is Relation-yielding means :: FUNCOP_1:def 11
for x being set st x in dom IT holds
IT . x is Relation;

end;

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

registration

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

coherence
for b₁ being Function st b₁ is Function-yielding holds
b₁ is Relation-yielding ;

end;

registration

cluster Relation-like Function-like empty -> Function-yielding for set ;

coherence
for b₁ being Function st b₁ is empty holds
b₁ is Function-yielding ;

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

proof end;

theorem Th88: :: FUNCOP_1:88

for x, y being set holds rng (x .--> y) = {y}

proof end;

theorem :: FUNCOP_1:89

for x, y, z, A being set st z in A holds
(A --> x) * (y .--> z) = y .--> x

proof end;

registration

let f be Function-yielding Function;
let a, b be object ;

cluster f . (a,b) -> Relation-like Function-like ;

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

end;

registration

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

cluster Function-like quasi_total -> Function-yielding for Element of bool [:X,(Funcs (Y,Z)):];

coherence
for b₁ being Function of X,(Funcs (Y,Z)) holds b₁ is Function-yielding ;

end;