:: FUNCOP_1 semantic presentation

theorem Th1: :: FUNCOP_1:1

for R being Relation
for A, B being set st A <> {} & B <> {} & R = [:A,B:] holds
( dom R = A & rng R = B )

proof end;

theorem Th2: :: FUNCOP_1:2

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

proof end;

theorem Th3: :: FUNCOP_1:3

for f, g, h being Function st dom f = dom g holds
dom (f * h) = dom (g * h)

proof end;

theorem :: FUNCOP_1:4

for f, g being Function st dom f = {} & dom g = {} holds
f = g

proof end;

definition

let f be Function;
func f ~ -> Function means :Def1: :: FUNCOP_1:def 1
( dom it = dom f & ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
it . x = [z,y] ) & ( f . x = it . x or ex y, z being set st f . x = [y,z] ) ) ) );
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :

theorem :: FUNCOP_1:5

canceled;

theorem Th6: :: FUNCOP_1:6

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

proof end;

theorem Th7: :: FUNCOP_1:7

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

proof end;

theorem :: FUNCOP_1:8

canceled;

theorem :: FUNCOP_1:9

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

proof end;

theorem Th10: :: FUNCOP_1:10

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

proof end;

theorem Th11: :: FUNCOP_1:11

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

proof end;

definition

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

end;

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

registration

let A, z be set ;
cluster A --> z -> Relation-like Function-like ;
coherence

proof end;

end;

theorem :: FUNCOP_1:12

canceled;

theorem Th13: :: FUNCOP_1:13

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

proof end;

theorem :: FUNCOP_1:14

for A, x being set st A <> {} holds
rng (A --> x) = {x} by Th1;

theorem Th15: :: FUNCOP_1:15

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

proof end;

registration

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

end;

registration

let x be set ;
let A be empty set ;
cluster A --> x -> empty Relation-like Function-like ;
coherence

proof end;

end;

theorem Th16: :: FUNCOP_1:16

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

theorem Th17: :: FUNCOP_1:17

for f being Function
for x being set st ( for z being set st z in dom f holds
f . z = x ) holds
f = (dom f) --> x

proof end;

theorem Th18: :: FUNCOP_1:18

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

proof end;

theorem Th19: :: FUNCOP_1:19

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

proof end;

theorem Th20: :: FUNCOP_1:20

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

proof end;

theorem :: FUNCOP_1:21

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

proof end;

theorem :: FUNCOP_1:22

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

proof end;

theorem :: FUNCOP_1:23

for h being Function
for A, x being set st x in dom h holds
h * (A --> x) = A --> (h . x)

proof end;

theorem :: FUNCOP_1:24

for h being Function
for A, x being set st A <> {} & x in dom h holds
dom (h * (A --> x)) <> {}

proof end;

theorem :: FUNCOP_1:25

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

proof end;

theorem :: FUNCOP_1:26

for A, x, y being set 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 ;

end;

:: deftheorem defines .: FUNCOP_1:def 3 :

registration

let F, f, g be Function;
cluster F .: f,g -> Relation-like Function-like ;
coherence ;

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)

proof end;

theorem :: FUNCOP_1:27

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

proof end;

theorem :: FUNCOP_1:28

for f, g, F being Function
for x being set st x in dom (F .: f,g) holds
(F .: f,g) . x = F . (f . x),(g . x) by Lm1;

theorem Th29: :: FUNCOP_1:29

for f, g, h being Function
for A being set
for F being Function st f | A = g | A holds
(F .: f,h) | A = (F .: g,h) | A

proof end;

theorem Th30: :: FUNCOP_1:30

for f, g, h being Function
for A being set
for F being Function st f | A = g | A holds
(F .: h,f) | A = (F .: h,g) | A

proof end;

theorem Th31: :: FUNCOP_1:31

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

proof end;

theorem :: FUNCOP_1:32

for h, f, g, F being Function holds h * (F .: f,g) = (h * F) .: f,g by RELAT_1:55;

definition

let F, f be Function;
let x be set ;
func F [:] f,x -> set equals :: FUNCOP_1:def 4
F * <:f,((dom f) --> x):>;
correctness ;

end;

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

registration

let F, f be Function;
let x be set ;
cluster F [:] f,x -> Relation-like Function-like ;
coherence ;

end;

theorem :: FUNCOP_1:33

canceled;

theorem :: FUNCOP_1:34

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

theorem Th35: :: FUNCOP_1:35

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

proof end;

theorem :: FUNCOP_1:36

for f, g being Function
for A being set
for F being Function
for x being set st f | A = g | A holds
(F [:] f,x) | A = (F [:] g,x) | A

proof end;

theorem Th37: :: FUNCOP_1:37

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

proof end;

theorem :: FUNCOP_1:38

for h, f, F being Function
for x being set holds h * (F [:] f,x) = (h * F) [:] f,x by RELAT_1:55;

theorem :: FUNCOP_1:39

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

proof end;

definition

let F be Function;
let x be set ;
let g be Function;
func F [;] x,g -> set equals :: FUNCOP_1:def 5
F * <:((dom g) --> x),g:>;
correctness ;

end;

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

registration

let F be Function;
let x be set ;
let g be Function;
cluster F [;] x,g -> Relation-like Function-like ;
coherence ;

end;

theorem :: FUNCOP_1:40

canceled;

theorem :: FUNCOP_1:41

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

theorem Th42: :: FUNCOP_1:42

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

proof end;

theorem :: FUNCOP_1:43

for f, g being Function
for A being set
for F being Function
for x being set st f | A = g | A holds
(F [;] x,f) | A = (F [;] x,g) | A

proof end;

theorem Th44: :: FUNCOP_1:44

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

proof end;

theorem :: FUNCOP_1:45

for h, f, F being Function
for x being set holds h * (F [;] x,f) = (h * F) [;] x,f by RELAT_1:55;

theorem :: FUNCOP_1:46

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

proof end;

theorem Th47: :: FUNCOP_1:47

for Y, X being non empty 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, Z be non empty 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 by Th47;

end;

theorem Th48: :: FUNCOP_1:48

for X, Y being non empty set
for F being BinOp of X
for f, g being Function of Y,X
for z being Element of Y holds (F .: f,g) . z = F . (f . z),(g . z)

proof end;

theorem Th49: :: FUNCOP_1:49

for Y, X 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:50

canceled;

theorem :: FUNCOP_1:51

for Y, X 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:52

for Y, X 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:53

for Y, X 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:54

for X being non empty set
for F being BinOp of X
for x being Element of X
for g being Function of X,X holds (F .: (id X),g) . x = F . x,(g . x)

proof end;

theorem :: FUNCOP_1:55

for X being non empty set
for F being BinOp of X
for x being Element of X
for g being Function of X,X holds (F .: g,(id X)) . x = F . (g . x),x

proof end;

theorem :: FUNCOP_1:56

for X being non empty set
for F being BinOp of X
for x being Element of X holds (F .: (id X),(id X)) . x = F . x,x

proof end;

theorem Th57: :: FUNCOP_1:57

for A, B, x being set st x in B holds
A --> x is Function of A,B

proof end;

theorem :: FUNCOP_1:58

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

theorem Th59: :: FUNCOP_1:59

for Y, X 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 [:] f,x is Function of Y,X

proof end;

definition

let X, Z be non empty 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 by Th59;

end;

theorem Th60: :: FUNCOP_1:60

for X, Y being non empty set
for F being BinOp of X
for f being Function of Y,X
for x being Element of X
for y being Element of Y holds (F [:] f,x) . y = F . (f . y),x

proof end;

theorem Th61: :: FUNCOP_1:61

for X, Y being non empty set
for F being BinOp of X
for g, f being Function of Y,X
for x being Element of X st ( for y being Element of Y holds g . y = F . (f . y),x ) holds
g = F [:] f,x

proof end;

theorem :: FUNCOP_1:62

canceled;

theorem :: FUNCOP_1:63

for Y, X 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:64

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

proof end;

theorem Th65: :: FUNCOP_1:65

for Y, X being non empty 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, Z be non empty 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 by Th65;

end;

theorem Th66: :: FUNCOP_1:66

for X, Y being non empty set
for F being BinOp of X
for f being Function of Y,X
for x being Element of X
for y being Element of Y holds (F [;] x,f) . y = F . x,(f . y)

proof end;

theorem Th67: :: FUNCOP_1:67

for X, Y being non empty set
for F being BinOp of X
for g, f being Function of Y,X
for x being Element of X st ( for y being Element of Y holds g . y = F . x,(f . y) ) holds
g = F [;] x,f

proof end;

theorem :: FUNCOP_1:68

canceled;

theorem :: FUNCOP_1:69

for Y, X 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 [;] x,(id X)) * f = F [;] x,f

proof end;

theorem :: FUNCOP_1:70

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

proof end;

theorem :: FUNCOP_1:71

for X, Y, Z being non empty set
for f being Function of X,[:Y,Z:]
for x being Element of X holds (f ~ ) . x = [((f . x) `2 ),((f . x) `1 )]

proof end;

theorem Th72: :: FUNCOP_1:72

for X, Y, Z being non empty set
for f being Function of X,[:Y,Z:] holds rng f is Relation of Y,Z

proof end;

definition

let X, Y, Z be non empty set ;
let f be Function of X,[:Y,Z:];
:: original: rng
redefine func rng f -> Relation of Y,Z;
coherence by Th72;

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

proof end;

end;

theorem :: FUNCOP_1:73

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

for Y, X being non empty set
for F being BinOp of X
for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [:] (F [;] x1,f),x2 = F [;] x1,(F [:] f,x2)

proof end;

theorem :: FUNCOP_1:75

for Y, X 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 F is associative holds
F .: (F [:] f,x),g = F .: f,(F [;] x,g)

proof end;

theorem :: FUNCOP_1:76

for Y, X being non empty set
for F being BinOp of X
for f, g, h being Function of Y,X st F is associative holds
F .: (F .: f,g),h = F .: f,(F .: g,h)

proof end;

theorem :: FUNCOP_1:77

for Y, X being non empty set
for F being BinOp of X
for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [;] (F . x1,x2),f = F [;] x1,(F [;] x2,f)

proof end;

theorem :: FUNCOP_1:78

for Y, X being non empty set
for F being BinOp of X
for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [:] f,(F . x1,x2) = F [:] (F [:] f,x1),x2

proof end;

theorem :: FUNCOP_1:79

for Y, X being non empty set
for F being BinOp of X
for f being Function of Y,X
for x being Element of X st F is commutative holds
F [;] x,f = F [:] f,x

proof end;

theorem :: FUNCOP_1:80

for Y, X being non empty set
for F being BinOp of X
for f, g being Function of Y,X st F is commutative holds
F .: f,g = F .: g,f

proof end;

theorem :: FUNCOP_1:81

for Y, X being non empty set
for F being BinOp of X
for f being Function of Y,X st F is idempotent holds
F .: f,f = f

proof end;

theorem :: FUNCOP_1:82

for X, Y being non empty set
for F being BinOp of X
for f being Function of Y,X
for y being Element of Y st F is idempotent holds
(F [;] (f . y),f) . y = f . y

proof end;

theorem :: FUNCOP_1:83

for X, Y being non empty set
for F being BinOp of X
for f being Function of Y,X
for y being Element of Y st F is idempotent holds
(F [:] f,(f . y)) . y = f . y

proof end;

theorem :: FUNCOP_1:84

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

proof end;

definition

let IT be Function;
attr IT is Function-yielding means :Def6: :: FUNCOP_1:def 6
for x being set st x in dom IT holds
IT . x is Function;

end;

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

registration

cluster Function-yielding set ;
existence

proof end;

end;

registration

let B be Function-yielding Function;
let j be set ;
cluster B . j -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let F be Function-yielding Function;
let f be Function;
cluster f * F -> Function-yielding ;
coherence

proof end;

end;

registration

let B be set ;
let c be non empty set ;
cluster B --> c -> Relation-like non-empty Function-like ;
coherence

proof end;

end;