:: FUNCOP_1 semantic presentation

theorem Th1: :: FUNCOP_1:1

for b₁ being Relation
for b₂, b₃ being set st b₂ <> {} & b₃ <> {} & b₁ = [:b₂,b₃:] holds
( dom b₁ = b₂ & rng b₁ = b₃ )

proof end;

theorem Th2: :: FUNCOP_1:2

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

proof end;

theorem Th3: :: FUNCOP_1:3

for b₁, b₂, b₃ being Function st dom b₁ = dom b₂ holds
dom (b₁ * b₃) = dom (b₂ * b₃)

proof end;

theorem Th4: :: FUNCOP_1:4

for b₁, b₂ being Function st dom b₁ = {} & dom b₂ = {} holds
b₁ = b₂

proof end;

definition

let c₁ be Function;
func c₁ ~ -> Function means :Def1: :: FUNCOP_1:def 1
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
( ( for b₂, b₃ being set st a₁ . b₁ = [b₂,b₃] holds
a₂ . b₁ = [b₃,b₂] ) & ( a₁ . b₁ = a₂ . b₁ or ex b₂, b₃ being set st a₁ . b₁ = [b₂,b₃] ) ) ) );
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :

theorem Th5: :: FUNCOP_1:5

canceled;

theorem Th6: :: FUNCOP_1:6

for b₁, b₂ being Function holds <:b₁,b₂:> = <:b₂,b₁:> ~

proof end;

theorem Th7: :: FUNCOP_1:7

for b₁ being Function
for b₂ being set holds (b₁ | b₂) ~ = (b₁ ~ ) | b₂

proof end;

theorem Th8: :: FUNCOP_1:8

canceled;

theorem Th9: :: FUNCOP_1:9

for b₁ being set holds (delta b₁) ~ = delta b₁

proof end;

theorem Th10: :: FUNCOP_1:10

for b₁, b₂ being Function
for b₃ being set holds <:b₁,b₂:> | b₃ = <:(b₁ | b₃),b₂:>

proof end;

theorem Th11: :: FUNCOP_1:11

for b₁, b₂ being Function
for b₃ being set holds <:b₁,b₂:> | b₃ = <:b₁,(b₂ | b₃):>

proof end;

definition

let c₁, c₂ be set ;
func c₁ --> c₂ -> set equals :: FUNCOP_1:def 2
[:a₁,{a₂}:];
coherence ;

end;

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

registration

let c₁, c₂ be set ;
cluster a₁ --> a₂ -> Relation-like Function-like ;
coherence

proof end;

end;

theorem Th12: :: FUNCOP_1:12

canceled;

theorem Th13: :: FUNCOP_1:13

for b₁, b₂, b₃ being set st b₂ in b₁ holds
(b₁ --> b₃) . b₂ = b₃

proof end;

theorem Th14: :: FUNCOP_1:14

for b₁, b₂ being set st b₁ <> {} holds
rng (b₁ --> b₂) = {b₂} by Th1;

theorem Th15: :: FUNCOP_1:15

for b₁ being Function
for b₂ being set st rng b₁ = {b₂} holds
b₁ = (dom b₁) --> b₂

proof end;

registration

let c₁ be set ;
cluster {} --> a₁ -> empty Relation-like Function-like ;
coherence by ZFMISC_1:113;

end;

registration

let c₁ be set ;
let c₂ be empty set ;
cluster a₂ --> a₁ -> empty Relation-like Function-like ;
coherence

proof end;

end;

theorem Th16: :: FUNCOP_1:16

for b₁ being set holds
( dom ({} --> b₁) = {} & rng ({} --> b₁) = {} ) ;

theorem Th17: :: FUNCOP_1:17

for b₁ being Function
for b₂ being set st ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ = b₂ ) holds
b₁ = (dom b₁) --> b₂

proof end;

theorem Th18: :: FUNCOP_1:18

for b₁, b₂, b₃ being set holds (b₁ --> b₂) | b₃ = (b₁ /\ b₃) --> b₂

proof end;

theorem Th19: :: FUNCOP_1:19

for b₁, b₂ being set holds
( dom (b₁ --> b₂) = b₁ & rng (b₁ --> b₂) c= {b₂} )

proof end;

theorem Th20: :: FUNCOP_1:20

for b₁, b₂, b₃ being set st b₂ in b₃ holds
(b₁ --> b₂) " b₃ = b₁

proof end;

theorem Th21: :: FUNCOP_1:21

for b₁, b₂ being set holds (b₁ --> b₂) " {b₂} = b₁

proof end;

theorem Th22: :: FUNCOP_1:22

for b₁, b₂, b₃ being set st not b₂ in b₃ holds
(b₁ --> b₂) " b₃ = {}

proof end;

theorem Th23: :: FUNCOP_1:23

for b₁ being Function
for b₂, b₃ being set st b₃ in dom b₁ holds
b₁ * (b₂ --> b₃) = b₂ --> (b₁ . b₃)

proof end;

theorem Th24: :: FUNCOP_1:24

for b₁ being Function
for b₂, b₃ being set st b₂ <> {} & b₃ in dom b₁ holds
dom (b₁ * (b₂ --> b₃)) <> {}

proof end;

theorem Th25: :: FUNCOP_1:25

for b₁ being Function
for b₂, b₃ being set holds (b₂ --> b₃) * b₁ = (b₁ " b₂) --> b₃

proof end;

theorem Th26: :: FUNCOP_1:26

for b₁, b₂, b₃ being set holds (b₁ --> [b₂,b₃]) ~ = b₁ --> [b₃,b₂]

proof end;

definition

let c₁, c₂, c₃ be Function;
func c₁ .: c₂,c₃ -> set equals :: FUNCOP_1:def 3
a₁ * <:a₂,a₃:>;
correctness ;

end;

:: deftheorem Def3 defines .: FUNCOP_1:def 3 :

registration

let c₁, c₂, c₃ be Function;
cluster a₁ .: a₂,a₃ -> Relation-like Function-like ;
coherence ;

end;

Lemma16: for b₁, b₂, b₃ being Function
for b₄ being set st b₄ in dom (b₃ * <:b₁,b₂:>) holds
(b₃ * <:b₁,b₂:>) . b₄ = b₃ . (b₁ . b₄),(b₂ . b₄)

proof end;

theorem Th27: :: FUNCOP_1:27

for b₁, b₂, b₃, b₄ being Function st dom b₄ = dom (b₃ .: b₁,b₂) & ( for b₅ being set st b₅ in dom (b₃ .: b₁,b₂) holds
b₄ . b₅ = b₃ . (b₁ . b₅),(b₂ . b₅) ) holds
b₄ = b₃ .: b₁,b₂

proof end;

theorem Th28: :: FUNCOP_1:28

for b₁, b₂, b₃ being Function
for b₄ being set st b₄ in dom (b₃ .: b₁,b₂) holds
(b₃ .: b₁,b₂) . b₄ = b₃ . (b₁ . b₄),(b₂ . b₄) by Lemma16;

theorem Th29: :: FUNCOP_1:29

for b₁, b₂, b₃ being Function
for b₄ being set
for b₅ being Function st b₁ | b₄ = b₂ | b₄ holds
(b₅ .: b₁,b₃) | b₄ = (b₅ .: b₂,b₃) | b₄

proof end;

theorem Th30: :: FUNCOP_1:30

for b₁, b₂, b₃ being Function
for b₄ being set
for b₅ being Function st b₁ | b₄ = b₂ | b₄ holds
(b₅ .: b₃,b₁) | b₄ = (b₅ .: b₃,b₂) | b₄

proof end;

theorem Th31: :: FUNCOP_1:31

for b₁, b₂, b₃, b₄ being Function holds (b₄ .: b₁,b₂) * b₃ = b₄ .: (b₁ * b₃),(b₂ * b₃)

proof end;

theorem Th32: :: FUNCOP_1:32

for b₁, b₂, b₃, b₄ being Function holds b₁ * (b₄ .: b₂,b₃) = (b₁ * b₄) .: b₂,b₃ by RELAT_1:55;

definition

let c₁, c₂ be Function;
let c₃ be set ;
func c₁ [:] c₂,c₃ -> set equals :: FUNCOP_1:def 4
a₁ * <:a₂,((dom a₂) --> a₃):>;
correctness ;

end;

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

registration

let c₁, c₂ be Function;
let c₃ be set ;
cluster a₁ [:] a₂,a₃ -> Relation-like Function-like ;
coherence ;

end;

theorem Th33: :: FUNCOP_1:33

canceled;

theorem Th34: :: FUNCOP_1:34

for b₁, b₂ being Function
for b₃ being set holds b₂ [:] b₁,b₃ = b₂ .: b₁,((dom b₁) --> b₃) ;

theorem Th35: :: FUNCOP_1:35

for b₁, b₂ being Function
for b₃, b₄ being set st b₃ in dom (b₂ [:] b₁,b₄) holds
(b₂ [:] b₁,b₄) . b₃ = b₂ . (b₁ . b₃),b₄

proof end;

theorem Th36: :: FUNCOP_1:36

for b₁, b₂ being Function
for b₃ being set
for b₄ being Function
for b₅ being set st b₁ | b₃ = b₂ | b₃ holds
(b₄ [:] b₁,b₅) | b₃ = (b₄ [:] b₂,b₅) | b₃

proof end;

theorem Th37: :: FUNCOP_1:37

for b₁, b₂, b₃ being Function
for b₄ being set holds (b₃ [:] b₁,b₄) * b₂ = b₃ [:] (b₁ * b₂),b₄

proof end;

theorem Th38: :: FUNCOP_1:38

for b₁, b₂, b₃ being Function
for b₄ being set holds b₁ * (b₃ [:] b₂,b₄) = (b₁ * b₃) [:] b₂,b₄ by RELAT_1:55;

theorem Th39: :: FUNCOP_1:39

for b₁ being Function
for b₂ being set
for b₃ being Function
for b₄ being set holds (b₃ [:] b₁,b₄) * (id b₂) = b₃ [:] (b₁ | b₂),b₄

proof end;

definition

let c₁ be Function;
let c₂ be set ;
let c₃ be Function;
func c₁ [;] c₂,c₃ -> set equals :: FUNCOP_1:def 5
a₁ * <:((dom a₃) --> a₂),a₃:>;
correctness ;

end;

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

registration

let c₁ be Function;
let c₂ be set ;
let c₃ be Function;
cluster a₁ [;] a₂,a₃ -> Relation-like Function-like ;
coherence ;

end;

theorem Th40: :: FUNCOP_1:40

canceled;

theorem Th41: :: FUNCOP_1:41

for b₁, b₂ being Function
for b₃ being set holds b₂ [;] b₃,b₁ = b₂ .: ((dom b₁) --> b₃),b₁ ;

theorem Th42: :: FUNCOP_1:42

for b₁, b₂ being Function
for b₃, b₄ being set st b₃ in dom (b₂ [;] b₄,b₁) holds
(b₂ [;] b₄,b₁) . b₃ = b₂ . b₄,(b₁ . b₃)

proof end;

theorem Th43: :: FUNCOP_1:43

for b₁, b₂ being Function
for b₃ being set
for b₄ being Function
for b₅ being set st b₁ | b₃ = b₂ | b₃ holds
(b₄ [;] b₅,b₁) | b₃ = (b₄ [;] b₅,b₂) | b₃

proof end;

theorem Th44: :: FUNCOP_1:44

for b₁, b₂, b₃ being Function
for b₄ being set holds (b₃ [;] b₄,b₁) * b₂ = b₃ [;] b₄,(b₁ * b₂)

proof end;

theorem Th45: :: FUNCOP_1:45

for b₁, b₂, b₃ being Function
for b₄ being set holds b₁ * (b₃ [;] b₄,b₂) = (b₁ * b₃) [;] b₄,b₂ by RELAT_1:55;

theorem Th46: :: FUNCOP_1:46

for b₁ being Function
for b₂ being set
for b₃ being Function
for b₄ being set holds (b₃ [;] b₄,b₁) * (id b₂) = b₃ [;] b₄,(b₁ | b₂)

proof end;

theorem Th47: :: FUNCOP_1:47

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄, b₅ being Function of b₁,b₂ holds b₃ .: b₄,b₅ is Function of b₁,b₂

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
let c₄, c₅ be Function of c₂,c₁;
redefine func .: as c₃ .: c₄,c₅ -> Function of a₂,a₁;
coherence by Th47;

end;

theorem Th48: :: FUNCOP_1:48

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄, b₅ being Function of b₂,b₁
for b₆ being Element of b₂ holds (b₃ .: b₄,b₅) . b₆ = b₃ . (b₄ . b₆),(b₅ . b₆)

proof end;

theorem Th49: :: FUNCOP_1:49

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄, b₅, b₆ being Function of b₁,b₂ st ( for b₇ being Element of b₁ holds b₆ . b₇ = b₃ . (b₄ . b₇),(b₅ . b₇) ) holds
b₆ = b₃ .: b₄,b₅

proof end;

theorem Th50: :: FUNCOP_1:50

canceled;

theorem Th51: :: FUNCOP_1:51

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₂ holds (b₃ .: (id b₂),b₅) * b₄ = b₃ .: b₄,(b₅ * b₄)

proof end;

theorem Th52: :: FUNCOP_1:52

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₂ holds (b₃ .: b₅,(id b₂)) * b₄ = b₃ .: (b₅ * b₄),b₄

proof end;

theorem Th53: :: FUNCOP_1:53

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂ holds (b₃ .: (id b₂),(id b₂)) * b₄ = b₃ .: b₄,b₄

proof end;

theorem Th54: :: FUNCOP_1:54

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃ being Element of b₁
for b₄ being Function of b₁,b₁ holds (b₂ .: (id b₁),b₄) . b₃ = b₂ . b₃,(b₄ . b₃)

proof end;

theorem Th55: :: FUNCOP_1:55

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃ being Element of b₁
for b₄ being Function of b₁,b₁ holds (b₂ .: b₄,(id b₁)) . b₃ = b₂ . (b₄ . b₃),b₃

proof end;

theorem Th56: :: FUNCOP_1:56

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃ being Element of b₁ holds (b₂ .: (id b₁),(id b₁)) . b₃ = b₂ . b₃,b₃

proof end;

theorem Th57: :: FUNCOP_1:57

for b₁, b₂, b₃ being set st b₃ in b₂ holds
b₁ --> b₃ is Function of b₁,b₂

proof end;

theorem Th58: :: FUNCOP_1:58

for b₁ being set
for b₂ being non empty set
for b₃ being Element of b₂ holds b₁ --> b₃ is Function of b₁,b₂ by Th57;

theorem Th59: :: FUNCOP_1:59

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂ holds b₃ [:] b₄,b₅ is Function of b₁,b₂

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
let c₄ be Function of c₂,c₁;
let c₅ be Element of c₁;
redefine func [:] as c₃ [:] c₄,c₅ -> Function of a₂,a₁;
coherence by Th59;

end;

theorem Th60: :: FUNCOP_1:60

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁
for b₅ being Element of b₁
for b₆ being Element of b₂ holds (b₃ [:] b₄,b₅) . b₆ = b₃ . (b₄ . b₆),b₅

proof end;

theorem Th61: :: FUNCOP_1:61

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄, b₅ being Function of b₂,b₁
for b₆ being Element of b₁ st ( for b₇ being Element of b₂ holds b₄ . b₇ = b₃ . (b₅ . b₇),b₆ ) holds
b₄ = b₃ [:] b₅,b₆

proof end;

theorem Th62: :: FUNCOP_1:62

canceled;

theorem Th63: :: FUNCOP_1:63

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂ holds (b₃ [:] (id b₂),b₅) * b₄ = b₃ [:] b₄,b₅

proof end;

theorem Th64: :: FUNCOP_1:64

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃ being Element of b₁ holds (b₂ [:] (id b₁),b₃) . b₃ = b₂ . b₃,b₃

proof end;

theorem Th65: :: FUNCOP_1:65

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂ holds b₃ [;] b₅,b₄ is Function of b₁,b₂

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
let c₄ be Element of c₁;
let c₅ be Function of c₂,c₁;
redefine func [;] as c₃ [;] c₄,c₅ -> Function of a₂,a₁;
coherence by Th65;

end;

theorem Th66: :: FUNCOP_1:66

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁
for b₅ being Element of b₁
for b₆ being Element of b₂ holds (b₃ [;] b₅,b₄) . b₆ = b₃ . b₅,(b₄ . b₆)

proof end;

theorem Th67: :: FUNCOP_1:67

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄, b₅ being Function of b₂,b₁
for b₆ being Element of b₁ st ( for b₇ being Element of b₂ holds b₄ . b₇ = b₃ . b₆,(b₅ . b₇) ) holds
b₄ = b₃ [;] b₆,b₅

proof end;

theorem Th68: :: FUNCOP_1:68

canceled;

theorem Th69: :: FUNCOP_1:69

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂ holds (b₃ [;] b₅,(id b₂)) * b₄ = b₃ [;] b₅,b₄

proof end;

theorem Th70: :: FUNCOP_1:70

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃ being Element of b₁ holds (b₂ [;] b₃,(id b₁)) . b₃ = b₂ . b₃,b₃

proof end;

theorem Th71: :: FUNCOP_1:71

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,[:b₂,b₃:]
for b₅ being Element of b₁ holds (b₄ ~ ) . b₅ = [((b₄ . b₅) `2 ),((b₄ . b₅) `1 )]

proof end;

theorem Th72: :: FUNCOP_1:72

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,[:b₂,b₃:] holds rng b₄ is Relation of b₂,b₃

proof end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of c₁,[:c₂,c₃:];
redefine func rng as rng c₄ -> Relation of a₂,a₃;
coherence by Th72;

end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of c₁,[:c₂,c₃:];
redefine func ~ as c₄ ~ -> Function of a₁,[:a₃,a₂:];
coherence

proof end;

end;

theorem Th73: :: FUNCOP_1:73

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,[:b₂,b₃:] holds rng (b₄ ~ ) = (rng b₄) ~

proof end;

theorem Th74: :: FUNCOP_1:74

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅, b₆ being Element of b₂ st b₃ is associative holds
b₃ [:] (b₃ [;] b₅,b₄),b₆ = b₃ [;] b₅,(b₃ [:] b₄,b₆)

proof end;

theorem Th75: :: FUNCOP_1:75

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄, b₅ being Function of b₁,b₂
for b₆ being Element of b₂ st b₃ is associative holds
b₃ .: (b₃ [:] b₄,b₆),b₅ = b₃ .: b₄,(b₃ [;] b₆,b₅)

proof end;

theorem Th76: :: FUNCOP_1:76

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄, b₅, b₆ being Function of b₁,b₂ st b₃ is associative holds
b₃ .: (b₃ .: b₄,b₅),b₆ = b₃ .: b₄,(b₃ .: b₅,b₆)

proof end;

theorem Th77: :: FUNCOP_1:77

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅, b₆ being Element of b₂ st b₃ is associative holds
b₃ [;] (b₃ . b₅,b₆),b₄ = b₃ [;] b₅,(b₃ [;] b₆,b₄)

proof end;

theorem Th78: :: FUNCOP_1:78

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅, b₆ being Element of b₂ st b₃ is associative holds
b₃ [:] b₄,(b₃ . b₅,b₆) = b₃ [:] (b₃ [:] b₄,b₅),b₆

proof end;

theorem Th79: :: FUNCOP_1:79

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂ st b₃ is commutative holds
b₃ [;] b₅,b₄ = b₃ [:] b₄,b₅

proof end;

theorem Th80: :: FUNCOP_1:80

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄, b₅ being Function of b₁,b₂ st b₃ is commutative holds
b₃ .: b₄,b₅ = b₃ .: b₅,b₄

proof end;

theorem Th81: :: FUNCOP_1:81

for b₁, b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂ st b₃ is idempotent holds
b₃ .: b₄,b₄ = b₄

proof end;

theorem Th82: :: FUNCOP_1:82

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁
for b₅ being Element of b₂ st b₃ is idempotent holds
(b₃ [;] (b₄ . b₅),b₄) . b₅ = b₄ . b₅

proof end;

theorem Th83: :: FUNCOP_1:83

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being Function of b₂,b₁
for b₅ being Element of b₂ st b₃ is idempotent holds
(b₃ [:] b₄,(b₄ . b₅)) . b₅ = b₄ . b₅

proof end;

theorem Th84: :: FUNCOP_1:84

for b₁, b₂, b₃ being Function st [:(rng b₂),(rng b₃):] c= dom b₁ holds
dom (b₁ .: b₂,b₃) = (dom b₂) /\ (dom b₃)

proof end;

definition

let c₁ be Function;
attr a₁ is Function-yielding means :Def6: :: FUNCOP_1:def 6
for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ is Function;

end;

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

registration

cluster Function-yielding set ;
existence

proof end;

end;

registration

let c₁ be Function-yielding Function;
let c₂ be set ;
cluster a₁ . a₂ -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let c₁ be Function-yielding Function;
let c₂ be Function;
cluster a₂ * a₁ -> Function-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster a₁ --> a₂ -> Relation-like non-empty Function-like ;
coherence

proof end;

end;