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


begin

theorem Th1: :: FUNCOP_1:1
for A being set holds delta A = <:(id A),(id A):>
proofend;

definition
let f be Function;
funcf ~  ->  Function means :Def1: :: FUNCOP_1:def 1
( dom it = dom f &amp; ( 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] ) &amp; ( f . x = it . x or ex y, z being set st f . x = [y,z] ) ) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b1 . x = [z,y] ) &amp; ( f . x = b1 . x or ex y, z being set st f . x = [y,z] ) ) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b1 . x = [z,y] ) &amp; ( f . x = b1 . x or ex y, z being set st f . x = [y,z] ) ) ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b2 . x = [z,y] ) &amp; ( f . x = b2 . x or ex y, z being set st f . x = [y,z] ) ) ) holds
b1 = b2
proofend;
involutiveness
 for b1, b2 being Function st dom b1 = dom b2 &amp; ( for x being set st x in dom b2 holds
( ( for y, z being set st b2 . x = [y,z] holds
b1 . x = [z,y] ) &amp; ( b2 . x = b1 . x or ex y, z being set st b2 . x = [y,z] ) ) ) holds
( dom b2 = dom b1 &amp; ( for x being set st x in dom b1 holds
( ( for y, z being set st b1 . x = [y,z] holds
b2 . x = [z,y] ) &amp; ( b1 . x = b2 . x or ex y, z being set st b1 . x = [y,z] ) ) ) )
proofend;
end;

:: deftheorem Def1 defines ~ FUNCOP_1:def_1_:_
 for f, b2 being Function holds
( b2 = f ~ iff ( dom b2 = dom f &amp; ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b2 . x = [z,y] ) &amp; ( f . x = b2 . x or ex y, z being set st f . x = [y,z] ) ) ) ) );

theorem Th2: :: FUNCOP_1:2
for f, g being Function holds <:f,g:> = <:g,f:> ~
proofend;

theorem Th3: :: FUNCOP_1:3
for f being Function
for A being set holds (f | A) ~ = (f ~) | A
proofend;

theorem :: FUNCOP_1:4
for A being set holds (delta A) ~ = delta A
proofend;

theorem Th5: :: FUNCOP_1:5
for f, g being Function
for A being set holds <:f,g:> | A = <:(f | A),g:>
proofend;

theorem Th6: :: FUNCOP_1:6
for f, g being Function
for A being set holds <:f,g:> | A = <:f,(g | A):>
proofend;

definition
let A, z be set ;
funcA --> z ->  set  equals :: FUNCOP_1:def 2
[:A,{z}:];
coherence
 [:A,{z}:] is set ;
end;

:: deftheorem  defines --> FUNCOP_1:def_2_:_
 for A, z being set holds A --> z = [:A,{z}:];

registration
let A, z be set ;
clusterA --> z ->  Relation-like Function-like ;
coherence
 ( A --> z is Function-like &amp; A --> z is Relation-like )
proofend;
end;

theorem Th7: :: FUNCOP_1:7
for A, x, z being set st x in A holds
(A --> z) . x = z
proofend;

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

theorem Th9: :: FUNCOP_1:9
for f being Function
for x being set st rng f = {x} holds
f = (dom f) --> x
proofend;

registration
let x be set ;
cluster{} --> x ->  empty ;
coherence
 {} --> x is empty by ZFMISC_1:90;
end;

registration
let x be set ;
let A be empty set ;
clusterA --> x ->  empty ;
coherence
 A --> x is empty ;
end;

registration
let x be set ;
let A be non empty set ;
clusterA --> x ->  non empty ;
coherence
 not A --> x is empty ;
end;

theorem :: FUNCOP_1:10
for x being set holds
( dom ({} --> x) = {} &amp; rng ({} --> x) = {} ) ;

theorem Th11: :: FUNCOP_1:11
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
proofend;

theorem Th12: :: FUNCOP_1:12
for A, x, B being set holds (A --> x) | B = (A /\ B) --> x
proofend;

theorem Th13: :: FUNCOP_1:13
for A, x being set holds
( dom (A --> x) = A &amp; rng (A --> x) c= {x} )
proofend;

theorem Th14: :: FUNCOP_1:14
for A, x, B being set st x in B holds
(A --> x) " B = A
proofend;

theorem :: FUNCOP_1:15
for A, x being set holds (A --> x) " {x} = A
proofend;

theorem :: FUNCOP_1:16
for A, x, B being set st not x in B holds
(A --> x) " B = {}
proofend;

theorem :: FUNCOP_1:17
for h being Function
for A, x being set st x in dom h holds
h * (A --> x) = A --> (h . x)
proofend;

theorem :: FUNCOP_1:18
for h being Function
for A, x being set st A <> {} &amp; x in dom h holds
dom (h * (A --> x)) <> {}
proofend;

theorem :: FUNCOP_1:19
for h being Function
for A, x being set holds (A --> x) * h = (h " A) --> x
proofend;

theorem :: FUNCOP_1:20
for A, x, y being set holds (A --> [x,y]) ~ = A --> [y,x]
proofend;

definition
let F, f, g be Function;
funcF .: (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;
clusterF .: (f,g) ->  Relation-like Function-like ;
coherence
 ( F .: (f,g) is Function-like &amp; F .: (f,g) is Relation-like ) ;
end;

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

theorem :: FUNCOP_1:21
for f, g, F, h being Function st dom h = dom (F .: (f,g)) &amp; ( for z being set st z in dom (F .: (f,g)) holds
h . z = F . ((f . z),(g . z)) ) holds
h = F .: (f,g)
proofend;

theorem :: FUNCOP_1:22
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;

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

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

theorem Th25: :: FUNCOP_1:25
for f, g, h, F being Function holds (F .: (f,g)) * h = F .: ((f * h),(g * h))
proofend;

definition
let F, f be Function;
let x be set ;
funcF [:] (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 set holds F [:] (f,x) = F * <:f,((dom f) --> x):>;

registration
let F, f be Function;
let x be set ;
clusterF [:] (f,x) ->  Relation-like Function-like ;
coherence
 ( F [:] (f,x) is Function-like &amp; F [:] (f,x) is Relation-like ) ;
end;

theorem :: FUNCOP_1:26
for f, F being Function
for x being set holds F [:] (f,x) = F .: (f,((dom f) --> x)) ;

theorem Th27: :: FUNCOP_1:27
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)
proofend;

theorem :: FUNCOP_1:28
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
proofend;

theorem Th29: :: FUNCOP_1:29
for f, h, F being Function
for x being set holds (F [:] (f,x)) * h = F [:] ((f * h),x)
proofend;

theorem :: FUNCOP_1:30
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)
proofend;

definition
let F be Function;
let x be set ;
let g be Function;
funcF [;] (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 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;
clusterF [;] (x,g) ->  Relation-like Function-like ;
coherence
 ( F [;] (x,g) is Function-like &amp; F [;] (x,g) is Relation-like ) ;
end;

theorem :: FUNCOP_1:31
for g, F being Function
for x being set holds F [;] (x,g) = F .: (((dom g) --> x),g) ;

theorem Th32: :: FUNCOP_1:32
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))
proofend;

theorem :: FUNCOP_1:33
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
proofend;

theorem Th34: :: FUNCOP_1:34
for f, h, F being Function
for x being set holds (F [;] (x,f)) * h = F [;] (x,(f * h))
proofend;

theorem :: FUNCOP_1:35
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))
proofend;

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

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 funcF .: (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))
proofend;

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

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

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

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

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

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

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

theorem Th45: :: FUNCOP_1:45
for A, B, x being set st x in B holds
A --> x is Function of A,B
proofend;

definition
let I, i be set ;
:: original:-->
redefine funcI --> i ->  Function of I,{i};
coherence
 I --> i is Function of I,{i}
proofend;
end;

definition
let B be non empty set ;
let A be set ;
let b be Element of B;
:: original:-->
redefine funcA --> 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
proofend;

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 funcF [:] (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)
proofend;

theorem Th49: :: FUNCOP_1:49
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)
proofend;

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

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

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

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 funcF [;] (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))
proofend;

theorem Th54: :: FUNCOP_1:54
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)
proofend;

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

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

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

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 funcf ~  ->  Function of X,[:Z,Y:];
coherence
 f ~ is Function of X,[:Z,Y:]
proofend;
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) ~
proofend;

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

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

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

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

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

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

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

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

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

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

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

:: from PRALG_1, 2004.07.23
definition
let IT be Function;
attrIT is Function-yielding  means :Def6: :: FUNCOP_1:def 6
 for x being set 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 set st x in dom IT holds
IT . x is Function );

registration
cluster Relation-like Function-like Function-yielding for set ;
existence
 ex b1 being Function st b1 is Function-yielding
proofend;
end;

registration
let B be Function-yielding Function;
let j be set ;
clusterB . j ->  Relation-like Function-like ;
coherence
 ( B . j is Function-like &amp; B . j is Relation-like )
proofend;
end;

registration
let F be Function-yielding Function;
let f be Function;
clusterf * F ->  Function-yielding ;
coherence
 F * f is Function-yielding
proofend;
end;

:: missing, 2005.11.13, A.T.
registration
let B be set ;
let c be non empty set ;
clusterB --> c ->  non-empty ;
coherence
 B --> c is non-empty
proofend;
end;

:: missing, 2005.12.20, A.T.
theorem :: FUNCOP_1:70
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
proofend;

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;

:: deftheorem  defines .--> FUNCOP_1:def_7_:_
 for a, b, c being set holds (a,b) .--> c = {[a,b]} --> c;

theorem :: FUNCOP_1:71
for a, b, c being set holds ((a,b) .--> c) . (a,b) = c
proofend;

:: from CQC_LANG, 2007.03.13, A.T.
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 ) &amp; ( not x = y implies b is set ) );
consistency
for b1 being set holds verum;
;
end;

:: 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 ) &amp; ( 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
proofend;
end;

definition
let x, y be set ;
funcx .--> 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 set holds x .--> y = {x} --> y;

registration
let x, y be set ;
clusterx .--> y ->  Relation-like Function-like ;
coherence
 ( x .--> y is Function-like &amp; x .--> y is Relation-like ) ;
end;

registration
let x, y be set ;
clusterx .--> y ->  one-to-one ;
coherence
 x .--> y is one-to-one
proofend;
end;

theorem Th72: :: FUNCOP_1:72
for x, y being set holds (x .--> y) . x = y
proofend;

:: from SCMFSA6A, 2007.07.22, A.T.
theorem :: FUNCOP_1:73
for a, b being set
for f being Function holds
( a .--> b c= f iff ( a in dom f &amp; f . a = b ) )
proofend;

notation
let o, m, r be set ;
synonym (o,m) :-> r for (o,m) .--> r;
end;

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

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

:: deftheorem  defines :-> FUNCOP_1:def_10_:_
 for o, m, r being set
for b4 being Function of [:{o},{m}:],{r} holds
( b4 = (o,m) :-> r iff verum );

theorem :: FUNCOP_1:74
for x, y being set holds x in dom (x .--> y)
proofend;

theorem :: FUNCOP_1:75
for z, x, y being set st z in dom (x .--> y) holds
z = x
proofend;

:: missing, 2008.04.15, A.T.
theorem :: FUNCOP_1:76
for A, x, y being set st not x in A holds
(x .--> y) | A = {}
proofend;

notation
let x, y be set ;
synonym x :-> y for x .--> y;
end;

definition
let m, o be set ;
:: original:.-->
redefine funcm :-> 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 ;
clusterf | C ->  Function-yielding ;
coherence
 f | C is Function-yielding
proofend;
end;

:: from CIRCCOMB, 2008.07.06, A.T.
registration
let A be set ;
let f be Function;
clusterA --> f ->  Function-yielding ;
coherence
 A --> f is Function-yielding
proofend;
end;

:: from SEQM_3, 2008.07.17, A.T.
registration
let X, a be set ;
clusterX --> a ->  constant ;
coherence
 X --> a is constant
proofend;
end;

:: from YELLOW_6, 2008.07.17, A.T.
registration
cluster Relation-like Function-like constant non empty for set ;
existence
 ex b1 being Function st
( not b1 is empty &amp; b1 is constant )
proofend;
end;

:: missing, 2008.07.17, A.T.
registration
let f be constant Function;
let X be set ;
clusterf | X ->  constant ;
coherence
 f | X is constant
proofend;
end;

:: missing, 2008.08.14, A.T.
theorem :: FUNCOP_1:78
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
proofend;

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

:: from CIRCCMB3, 2008.12.26, A.T.
theorem :: FUNCOP_1:80
for f being constant Function holds f = (dom f) --> (the_value_of f)
proofend;

:: 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 b1 being PartFunc of X,Y st b1 is total
proofend;
end;

:: new, 2009.02.14, A.T.
registration
let I, A be set ;
clusterI --> A -> I -defined ;
coherence
 I --> A is I -defined ;
end;

registration
let I, A be set ;
clusterI .--> 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, x being set holds (A --> x) .: B c= {x} ;

registration
let I be set ;
let f be Function;
clusterI .--> 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 b1 being non-empty I -defined Function st b1 is total
proofend;
end;

theorem Th82: :: FUNCOP_1:82
for x, y being set holds x .--> y is_isomorphism_of {[x,x]},{[y,y]}
proofend;

theorem :: FUNCOP_1:83
for x, y being set holds {[x,x]},{[y,y]} are_isomorphic
proofend;

registration
let I, A be set ;
clusterI --> A -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = I --> A holds
b1 is total ;
end;

theorem :: FUNCOP_1:84
for x being set
for f being Function st x in dom f holds
x .--> (f . x) c= f
proofend;

registration
let A be non empty set ;
let x be set ;
let i be Element of A;
clusterx .--> i -> A -valued ;
coherence
 x .--> i is A -valued
proofend;
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)))
proofend;

registration
let A be set ;
let B be non empty set ;
let x be Element of B;
clusterA --> 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 set ;
clusterx .--> y -> A -defined ;
coherence
 x .--> y is A -defined
proofend;
end;

theorem :: FUNCOP_1:86
for x, y, A being set st x in A holds
(x .--> y) | A = x .--> y
proofend;

:: 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 b1 being Function st b1 is Y -valued holds
b1 is Function-yielding
proofend;
end;

:: from MSUALG_4, 2011.04.16, A.T.
definition
let IT be Function;
attrIT 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 b1 being Function st b1 is Function-yielding holds
b1 is Relation-yielding
proofend;
end;

registration
cluster Relation-like Function-like empty  ->  Function-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is Function-yielding
proofend;
end;

:: from CIRCCOMB, 2011.04.19, A.T.
theorem :: FUNCOP_1:87
for X, Y, x, y being set holds
( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )
proofend;

theorem Th88: :: FUNCOP_1:88
for x, y being set holds rng (x .--> y) = {y}
proofend;

theorem :: FUNCOP_1:89
for z, A, x, y being set st z in A holds
(A --> x) * (y .--> z) = y .--> x
proofend;