:: FUNCT_2 semantic presentation

definition

let c₁, c₂ be set ;
let c₃ be Relation of c₁,c₂;
attr a₃ is quasi_total means :Def1: :: FUNCT_2:def 1
a₁ = dom a₃ if ( a₂ = {} implies a₁ = {} )
otherwise a₃ = {} ;
consistency ;

end;

:: deftheorem Def1 defines quasi_total FUNCT_2:def 1 :

registration

let c₁, c₂ be set ;
cluster Function-like quasi_total Relation of a₁,a₂;
existence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster total -> quasi_total Relation of a₁,a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
mode Function of a₁,a₂ is Function-like quasi_total Relation of a₁,a₂;

end;

theorem Th1: :: FUNCT_2:1

canceled;

theorem Th2: :: FUNCT_2:2

canceled;

theorem Th3: :: FUNCT_2:3

for b₁ being Function holds b₁ is Function of dom b₁, rng b₁

proof end;

theorem Th4: :: FUNCT_2:4

for b₁ being set
for b₂ being Function st rng b₂ c= b₁ holds
b₂ is Function of dom b₂,b₁

proof end;

theorem Th5: :: FUNCT_2:5

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

proof end;

theorem Th6: :: FUNCT_2:6

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} & b₃ in b₁ holds
b₄ . b₃ in rng b₄

proof end;

theorem Th7: :: FUNCT_2:7

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} & b₃ in b₁ holds
b₄ . b₃ in b₂

proof end;

theorem Th8: :: FUNCT_2:8

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & rng b₄ c= b₃ holds
b₄ is Function of b₁,b₃

proof end;

theorem Th9: :: FUNCT_2:9

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₂ c= b₃ holds
b₄ is Function of b₁,b₃

proof end;

scheme :: FUNCT_2:sch 1
s1{ F₁() -> set , F₂() -> set , P₁[ set , set ] } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being set st b₂ in F₁() holds
P₁[b₂,b₁ . b₂]

provided

E5: for b₁ being set st b₁ in F₁() holds
ex b₂ being set st
( b₂ in F₂() & P₁[b₁,b₂] )

proof end;

scheme :: FUNCT_2:sch 2
s2{ F₁() -> set , F₂() -> set , F₃( set ) -> set } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being set st b₂ in F₁() holds
b₁ . b₂ = F₃(b₂)

provided

E5: for b₁ being set st b₁ in F₁() holds
F₃(b₁) in F₂()

proof end;

definition

let c₁, c₂ be set ;
func Funcs c₁,c₂ -> set means :Def2: :: FUNCT_2:def 2
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Function st
( b₁ = b₂ & dom b₂ = a₁ & rng b₂ c= a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Funcs FUNCT_2:def 2 :

theorem Th10: :: FUNCT_2:10

canceled;

theorem Th11: :: FUNCT_2:11

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
b₃ in Funcs b₁,b₂

proof end;

theorem Th12: :: FUNCT_2:12

for b₁ being set
for b₂ being Function of b₁,b₁ holds b₂ in Funcs b₁,b₁

proof end;

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster Funcs a₁,a₂ -> non empty ;
coherence by Th11;

end;

registration

let c₁ be set ;
cluster Funcs a₁,a₁ -> non empty ;
coherence by Th12;

end;

theorem Th13: :: FUNCT_2:13

canceled;

theorem Th14: :: FUNCT_2:14

for b₁ being set st b₁ <> {} holds
Funcs b₁,{} = {}

proof end;

theorem Th15: :: FUNCT_2:15

canceled;

theorem Th16: :: FUNCT_2:16

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₂ <> {} & ( for b₄ being set st b₄ in b₂ holds
ex b₅ being set st
( b₅ in b₁ & b₄ = b₃ . b₅ ) ) holds
rng b₃ = b₂

proof end;

theorem Th17: :: FUNCT_2:17

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₃ in b₂ & rng b₄ = b₂ holds
ex b₅ being set st
( b₅ in b₁ & b₄ . b₅ = b₃ )

proof end;

theorem Th18: :: FUNCT_2:18

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

proof end;

theorem Th19: :: FUNCT_2:19

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st ( not b₂ = {} or b₃ = {} or b₁ = {} ) holds
b₅ * b₄ is Function of b₁,b₃

proof end;

theorem Th20: :: FUNCT_2:20

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₂ <> {} & b₃ <> {} & rng b₄ = b₂ & rng b₅ = b₃ holds
rng (b₅ * b₄) = b₃

proof end;

theorem Th21: :: FUNCT_2:21

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function st b₂ <> {} & b₃ in b₁ holds
(b₅ * b₄) . b₃ = b₅ . (b₄ . b₃)

proof end;

theorem Th22: :: FUNCT_2:22

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₂ <> {} holds
( rng b₃ = b₂ iff for b₄ being set st b₄ <> {} holds
for b₅, b₆ being Function of b₂,b₄ st b₅ * b₃ = b₆ * b₃ holds
b₅ = b₆ )

proof end;

theorem Th23: :: FUNCT_2:23

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds
( (id b₁) * b₃ = b₃ & b₃ * (id b₂) = b₃ )

proof end;

theorem Th24: :: FUNCT_2:24

for b₁, b₂ being set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ * b₄ = id b₂ holds
rng b₃ = b₂

proof end;

theorem Th25: :: FUNCT_2:25

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
( b₃ is one-to-one iff for b₄, b₅ being set st b₄ in b₁ & b₅ in b₁ & b₃ . b₄ = b₃ . b₅ holds
b₄ = b₅ )

proof end;

theorem Th26: :: FUNCT_2:26

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st ( b₃ = {} implies b₂ = {} ) & ( b₂ = {} implies b₁ = {} ) & b₅ * b₄ is one-to-one holds
b₄ is one-to-one

proof end;

theorem Th27: :: FUNCT_2:27

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₁ <> {} & b₂ <> {} holds
( b₃ is one-to-one iff for b₄ being set
for b₅, b₆ being Function of b₄,b₁ st b₃ * b₅ = b₃ * b₆ holds
b₅ = b₆ )

proof end;

theorem Th28: :: FUNCT_2:28

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₃ <> {} & rng (b₅ * b₄) = b₃ & b₅ is one-to-one holds
rng b₄ = b₂

proof end;

theorem Th29: :: FUNCT_2:29

for b₁, b₂ being set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₂ <> {} & b₄ * b₃ = id b₁ holds
( b₃ is one-to-one & rng b₄ = b₁ )

proof end;

theorem Th30: :: FUNCT_2:30

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st ( b₃ = {} implies b₂ = {} ) & b₅ * b₄ is one-to-one & rng b₄ = b₂ holds
( b₄ is one-to-one & b₅ is one-to-one )

proof end;

theorem Th31: :: FUNCT_2:31

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₃ is one-to-one & rng b₃ = b₂ holds
b₃ " is Function of b₂,b₁

proof end;

theorem Th32: :: FUNCT_2:32

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} & b₄ is one-to-one & b₃ in b₁ holds
(b₄ " ) . (b₄ . b₃) = b₃

proof end;

theorem Th33: :: FUNCT_2:33

canceled;

theorem Th34: :: FUNCT_2:34

for b₁, b₂ being set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₁ <> {} & b₂ <> {} & rng b₃ = b₂ & b₃ is one-to-one & ( for b₅, b₆ being set holds
( b₅ in b₂ & b₄ . b₅ = b₆ iff ( b₆ in b₁ & b₃ . b₆ = b₅ ) ) ) holds
b₄ = b₃ "

proof end;

theorem Th35: :: FUNCT_2:35

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₂ <> {} & rng b₃ = b₂ & b₃ is one-to-one holds
( (b₃ " ) * b₃ = id b₁ & b₃ * (b₃ " ) = id b₂ )

proof end;

theorem Th36: :: FUNCT_2:36

for b₁, b₂ being set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₁ <> {} & b₂ <> {} & rng b₃ = b₂ & b₄ * b₃ = id b₁ & b₃ is one-to-one holds
b₄ = b₃ "

proof end;

theorem Th37: :: FUNCT_2:37

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₂ <> {} & ex b₄ being Function of b₂,b₁ st b₄ * b₃ = id b₁ holds
b₃ is one-to-one

proof end;

theorem Th38: :: FUNCT_2:38

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ c= b₁ holds
b₄ | b₃ is Function of b₃,b₂

proof end;

theorem Th39: :: FUNCT_2:39

canceled;

theorem Th40: :: FUNCT_2:40

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₁ c= b₃ holds
b₄ | b₃ = b₄

proof end;

theorem Th41: :: FUNCT_2:41

for b₁, b₂, b₃, b₄ being set
for b₅ being Function of b₁,b₂ st b₂ <> {} & b₃ in b₁ & b₅ . b₃ in b₄ holds
(b₄ | b₅) . b₃ = b₅ . b₃

proof end;

theorem Th42: :: FUNCT_2:42

canceled;

theorem Th43: :: FUNCT_2:43

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} holds
for b₅ being set st ex b₆ being set st
( b₆ in b₁ & b₆ in b₃ & b₅ = b₄ . b₆ ) holds
b₅ in b₄ .: b₃

proof end;

theorem Th44: :: FUNCT_2:44

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ holds b₄ .: b₃ c= b₂

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
redefine func .: as c₃ .: c₄ -> Subset of a₂;
coherence by Th44;

end;

theorem Th45: :: FUNCT_2:45

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
b₃ .: b₁ = rng b₃

proof end;

theorem Th46: :: FUNCT_2:46

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} holds
for b₅ being set holds
( b₅ in b₄ " b₃ iff ( b₅ in b₁ & b₄ . b₅ in b₃ ) )

proof end;

theorem Th47: :: FUNCT_2:47

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ holds b₄ " b₃ c= b₁

proof end;

definition

let c₁, c₂ be set ;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
redefine func " as c₃ " c₄ -> Subset of a₁;
coherence by Th47;

end;

theorem Th48: :: FUNCT_2:48

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
b₃ " b₂ = b₁

proof end;

theorem Th49: :: FUNCT_2:49

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ holds
( ( for b₄ being set st b₄ in b₂ holds
b₃ " {b₄} <> {} ) iff rng b₃ = b₂ )

proof end;

theorem Th50: :: FUNCT_2:50

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ c= b₁ holds
b₃ c= b₄ " (b₄ .: b₃)

proof end;

theorem Th51: :: FUNCT_2:51

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
b₃ " (b₃ .: b₁) = b₁

proof end;

theorem Th52: :: FUNCT_2:52

canceled;

theorem Th53: :: FUNCT_2:53

for b₁, b₂, b₃, b₄ being set
for b₅ being Function of b₁,b₂
for b₆ being Function of b₂,b₃ st ( b₃ = {} implies b₂ = {} ) & ( b₂ = {} implies b₁ = {} ) holds
b₅ " b₄ c= (b₆ * b₅) " (b₆ .: b₄)

proof end;

theorem Th54: :: FUNCT_2:54

canceled;

theorem Th55: :: FUNCT_2:55

for b₁ being set
for b₂ being Function st dom b₂ = {} holds
b₂ is Function of {} ,b₁

proof end;

theorem Th56: :: FUNCT_2:56

canceled;

theorem Th57: :: FUNCT_2:57

canceled;

theorem Th58: :: FUNCT_2:58

canceled;

theorem Th59: :: FUNCT_2:59

for b₁, b₂ being set
for b₃ being Function of {} ,b₁ holds b₃ .: b₂ = {}

proof end;

theorem Th60: :: FUNCT_2:60

for b₁, b₂ being set
for b₃ being Function of {} ,b₁ holds b₃ " b₂ = {}

proof end;

theorem Th61: :: FUNCT_2:61

for b₁, b₂ being set
for b₃ being Function of {b₁},b₂ st b₂ <> {} holds
b₃ . b₁ in b₂

proof end;

theorem Th62: :: FUNCT_2:62

for b₁, b₂ being set
for b₃ being Function of {b₁},b₂ st b₂ <> {} holds
rng b₃ = {(b₃ . b₁)}

proof end;

theorem Th63: :: FUNCT_2:63

canceled;

theorem Th64: :: FUNCT_2:64

for b₁, b₂, b₃ being set
for b₄ being Function of {b₁},b₂ st b₂ <> {} holds
b₄ .: b₃ c= {(b₄ . b₁)}

proof end;

theorem Th65: :: FUNCT_2:65

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,{b₂} st b₃ in b₁ holds
b₄ . b₃ = b₂

proof end;

theorem Th66: :: FUNCT_2:66

for b₁, b₂ being set
for b₃, b₄ being Function of b₁,{b₂} holds b₃ = b₄

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Function of c₁,c₁;
redefine func * as c₃ * c₂ -> Function of a₁,a₁;
coherence

proof end;

end;

theorem Th67: :: FUNCT_2:67

for b₁ being set
for b₂ being Function of b₁,b₁ holds
( dom b₂ = b₁ & rng b₂ c= b₁ )

proof end;

theorem Th68: :: FUNCT_2:68

canceled;

theorem Th69: :: FUNCT_2:69

canceled;

theorem Th70: :: FUNCT_2:70

for b₁, b₂ being set
for b₃ being Function of b₁,b₁
for b₄ being Function st b₂ in b₁ holds
(b₄ * b₃) . b₂ = b₄ . (b₃ . b₂)

proof end;

theorem Th71: :: FUNCT_2:71

canceled;

theorem Th72: :: FUNCT_2:72

canceled;

theorem Th73: :: FUNCT_2:73

for b₁ being set
for b₂, b₃ being Function of b₁,b₁ st rng b₂ = b₁ & rng b₃ = b₁ holds
rng (b₃ * b₂) = b₁

proof end;

theorem Th74: :: FUNCT_2:74

for b₁ being set
for b₂ being Relation of b₁,b₁ holds
( b₂ * (id b₁) = b₂ & (id b₁) * b₂ = b₂ ) by Th23;

theorem Th75: :: FUNCT_2:75

for b₁ being set
for b₂, b₃ being Function of b₁,b₁ st b₃ * b₂ = b₂ & rng b₂ = b₁ holds
b₃ = id b₁

proof end;

theorem Th76: :: FUNCT_2:76

for b₁ being set
for b₂, b₃ being Function of b₁,b₁ st b₂ * b₃ = b₂ & b₂ is one-to-one holds
b₃ = id b₁

proof end;

theorem Th77: :: FUNCT_2:77

for b₁ being set
for b₂ being Function of b₁,b₁ holds
( b₂ is one-to-one iff for b₃, b₄ being set st b₃ in b₁ & b₄ in b₁ & b₂ . b₃ = b₂ . b₄ holds
b₃ = b₄ )

proof end;

theorem Th78: :: FUNCT_2:78

canceled;

theorem Th79: :: FUNCT_2:79

for b₁ being set
for b₂ being Function of b₁,b₁ holds b₂ .: b₁ = rng b₂

proof end;

theorem Th80: :: FUNCT_2:80

canceled;

theorem Th81: :: FUNCT_2:81

canceled;

theorem Th82: :: FUNCT_2:82

for b₁ being set
for b₂ being Function of b₁,b₁ holds b₂ " (b₂ .: b₁) = b₁

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
attr a₃ is onto means :Def3: :: FUNCT_2:def 3
rng a₃ = a₂;

end;

:: deftheorem Def3 defines onto FUNCT_2:def 3 :

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
attr a₃ is bijective means :Def4: :: FUNCT_2:def 4
( a₃ is one-to-one & a₃ is onto );

end;

:: deftheorem Def4 defines bijective FUNCT_2:def 4 :

registration

let c₁, c₂ be set ;
cluster bijective -> one-to-one onto Relation of a₁,a₂;
coherence by Def4;
cluster one-to-one onto -> bijective Relation of a₁,a₂;
coherence by Def4;

end;

registration

let c₁ be set ;
cluster one-to-one onto bijective Relation of a₁,a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode Permutation of a₁ is bijective Function of a₁,a₁;

end;

theorem Th83: :: FUNCT_2:83

for b₁ being set
for b₂ being Function of b₁,b₁ st b₂ is one-to-one & rng b₂ = b₁ holds
b₂ is Permutation of b₁

proof end;

theorem Th84: :: FUNCT_2:84

canceled;

theorem Th85: :: FUNCT_2:85

for b₁ being set
for b₂ being Function of b₁,b₁ st b₂ is one-to-one holds
for b₃, b₄ being set st b₃ in b₁ & b₄ in b₁ & b₂ . b₃ = b₂ . b₄ holds
b₃ = b₄ by Th77;

definition

let c₁ be set ;
let c₂, c₃ be Permutation of c₁;
redefine func * as c₃ * c₂ -> Permutation of a₁;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster total reflexive -> one-to-one onto bijective Relation of a₁,a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Permutation of c₁;
redefine func " as c₂ " -> Permutation of a₁;
coherence

proof end;

end;

theorem Th86: :: FUNCT_2:86

for b₁ being set
for b₂, b₃ being Permutation of b₁ st b₃ * b₂ = b₃ holds
b₂ = id b₁

proof end;

theorem Th87: :: FUNCT_2:87

for b₁ being set
for b₂, b₃ being Permutation of b₁ st b₃ * b₂ = id b₁ holds
b₃ = b₂ "

proof end;

theorem Th88: :: FUNCT_2:88

for b₁ being set
for b₂ being Permutation of b₁ holds
( (b₂ " ) * b₂ = id b₁ & b₂ * (b₂ " ) = id b₁ )

proof end;

theorem Th89: :: FUNCT_2:89

canceled;

theorem Th90: :: FUNCT_2:90

canceled;

theorem Th91: :: FUNCT_2:91

canceled;

theorem Th92: :: FUNCT_2:92

for b₁, b₂ being set
for b₃ being Permutation of b₁ st b₂ c= b₁ holds
( b₃ .: (b₃ " b₂) = b₂ & b₃ " (b₃ .: b₂) = b₂ )

proof end;

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster quasi_total -> total quasi_total Relation of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be set ;
let c₄ be Function of c₁,c₂;
let c₅ be Function of c₂,c₃;
redefine func * as c₅ * c₄ -> Function of a₁,a₃;
coherence by Th19;

end;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Function of c₁,c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

scheme :: FUNCT_2:sch 3
s3{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being Element of F₁() holds P₁[b₂,b₁ . b₂]

provided

E27: for b₁ being Element of F₁() ex b₂ being Element of F₂() st P₁[b₁,b₂]

proof end;

scheme :: FUNCT_2:sch 4
s4{ F₁() -> non empty set , F₂() -> non empty set , F₃( Element of F₁()) -> Element of F₂() } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being Element of F₁() holds b₁ . b₂ = F₃(b₂)

proof end;

theorem Th93: :: FUNCT_2:93

canceled;

theorem Th94: :: FUNCT_2:94

canceled;

theorem Th95: :: FUNCT_2:95

canceled;

theorem Th96: :: FUNCT_2:96

canceled;

theorem Th97: :: FUNCT_2:97

canceled;

theorem Th98: :: FUNCT_2:98

canceled;

theorem Th99: :: FUNCT_2:99

canceled;

theorem Th100: :: FUNCT_2:100

canceled;

theorem Th101: :: FUNCT_2:101

canceled;

theorem Th102: :: FUNCT_2:102

canceled;

theorem Th103: :: FUNCT_2:103

canceled;

theorem Th104: :: FUNCT_2:104

canceled;

theorem Th105: :: FUNCT_2:105

canceled;

theorem Th106: :: FUNCT_2:106

canceled;

theorem Th107: :: FUNCT_2:107

canceled;

theorem Th108: :: FUNCT_2:108

canceled;

theorem Th109: :: FUNCT_2:109

canceled;

theorem Th110: :: FUNCT_2:110

canceled;

theorem Th111: :: FUNCT_2:111

canceled;

theorem Th112: :: FUNCT_2:112

canceled;

theorem Th113: :: FUNCT_2:113

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

proof end;

theorem Th114: :: FUNCT_2:114

canceled;

theorem Th115: :: FUNCT_2:115

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

proof end;

theorem Th116: :: FUNCT_2:116

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

proof end;

theorem Th117: :: FUNCT_2:117

canceled;

theorem Th118: :: FUNCT_2:118

for b₁, b₂, b₃ being set
for b₄, b₅ being Function of [:b₁,b₂:],b₃ st ( for b₆, b₇ being set st b₆ in b₁ & b₇ in b₂ holds
b₄ . [b₆,b₇] = b₅ . [b₆,b₇] ) holds
b₄ = b₅

proof end;

theorem Th119: :: FUNCT_2:119

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Function of [:b₁,b₂:],b₃ st b₄ in b₁ & b₅ in b₂ & b₃ <> {} holds
b₆ . [b₄,b₅] in b₃

proof end;

scheme :: FUNCT_2:sch 5
s5{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

ex b₁ being Function of [:F₁(),F₂():],F₃() st
for b₂, b₃ being set st b₂ in F₁() & b₃ in F₂() holds
P₁[b₂,b₃,b₁ . [b₂,b₃]]

provided

E29: for b₁, b₂ being set st b₁ in F₁() & b₂ in F₂() holds
ex b₃ being set st
( b₃ in F₃() & P₁[b₁,b₂,b₃] )

proof end;

scheme :: FUNCT_2:sch 6
s6{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set } :

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

provided

E29: for b₁, b₂ being set st b₁ in F₁() & b₂ in F₂() holds
F₄(b₁,b₂) in F₃()

proof end;

theorem Th120: :: FUNCT_2:120

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

proof end;

scheme :: FUNCT_2:sch 7
s7{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , P₁[ set , set , set ] } :

ex b₁ being Function of [:F₁(),F₂():],F₃() st
for b₂ being Element of F₁()
for b₃ being Element of F₂() holds P₁[b₂,b₃,b₁ . [b₂,b₃]]

provided

E29: for b₁ being Element of F₁()
for b₂ being Element of F₂() ex b₃ being Element of F₃() st P₁[b₁,b₂,b₃]

proof end;

scheme :: FUNCT_2:sch 8
s8{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( Element of F₁(), Element of F₂()) -> Element of F₃() } :

ex b₁ being Function of [:F₁(),F₂():],F₃() st
for b₂ being Element of F₁()
for b₃ being Element of F₂() holds b₁ . [b₂,b₃] = F₄(b₂,b₃)

proof end;

theorem Th121: :: FUNCT_2:121

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

proof end;

scheme :: FUNCT_2:sch 9
s9{ F₁() -> set , F₂() -> set , P₁[ set ], F₃( set ) -> set , F₄( set ) -> set } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being set st b₂ in F₁() holds
( ( P₁[b₂] implies b₁ . b₂ = F₃(b₂) ) & ( P₁[b₂] implies b₁ . b₂ = F₄(b₂) ) )

provided

E30: for b₁ being set st b₁ in F₁() holds
( ( P₁[b₁] implies F₃(b₁) in F₂() ) & ( P₁[b₁] implies F₄(b₁) in F₂() ) )

proof end;

theorem Th122: :: FUNCT_2:122

canceled;

theorem Th123: :: FUNCT_2:123

canceled;

theorem Th124: :: FUNCT_2:124

canceled;

theorem Th125: :: FUNCT_2:125

canceled;

theorem Th126: :: FUNCT_2:126

canceled;

theorem Th127: :: FUNCT_2:127

canceled;

theorem Th128: :: FUNCT_2:128

canceled;

theorem Th129: :: FUNCT_2:129

canceled;

theorem Th130: :: FUNCT_2:130

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st dom b₃ = b₁ holds
b₃ is Function of b₁,b₂

proof end;

theorem Th131: :: FUNCT_2:131

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st b₃ is total holds
b₃ is Function of b₁,b₂

proof end;

theorem Th132: :: FUNCT_2:132

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ is Function of b₁,b₂ holds
b₃ is total

proof end;

theorem Th133: :: FUNCT_2:133

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
<:b₃,b₁,b₂:> is total

proof end;

theorem Th134: :: FUNCT_2:134

for b₁ being set
for b₂ being Function of b₁,b₁ holds <:b₂,b₁,b₁:> is total

proof end;

theorem Th135: :: FUNCT_2:135

canceled;

theorem Th136: :: FUNCT_2:136

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
ex b₄ being Function of b₁,b₂ st
for b₅ being set st b₅ in dom b₃ holds
b₄ . b₅ = b₃ . b₅

proof end;

theorem Th137: :: FUNCT_2:137

canceled;

theorem Th138: :: FUNCT_2:138

canceled;

theorem Th139: :: FUNCT_2:139

canceled;

theorem Th140: :: FUNCT_2:140

canceled;

theorem Th141: :: FUNCT_2:141

for b₁, b₂ being set holds Funcs b₁,b₂ c= PFuncs b₁,b₂

proof end;

theorem Th142: :: FUNCT_2:142

for b₁, b₂ being set
for b₃, b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ tolerates b₄ holds
b₃ = b₄

proof end;

theorem Th143: :: FUNCT_2:143

for b₁ being set
for b₂, b₃ being Function of b₁,b₁ st b₂ tolerates b₃ holds
b₂ = b₃

proof end;

theorem Th144: :: FUNCT_2:144

canceled;

theorem Th145: :: FUNCT_2:145

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
( b₃ tolerates b₄ iff for b₅ being set st b₅ in dom b₃ holds
b₃ . b₅ = b₄ . b₅ )

proof end;

theorem Th146: :: FUNCT_2:146

for b₁ being set
for b₂ being PartFunc of b₁,b₁
for b₃ being Function of b₁,b₁ holds
( b₂ tolerates b₃ iff for b₄ being set st b₄ in dom b₂ holds
b₂ . b₄ = b₃ . b₄ )

proof end;

theorem Th147: :: FUNCT_2:147

canceled;

theorem Th148: :: FUNCT_2:148

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
ex b₄ being Function of b₁,b₂ st b₃ tolerates b₄

proof end;

theorem Th149: :: FUNCT_2:149

for b₁ being set
for b₂ being PartFunc of b₁,b₁ ex b₃ being Function of b₁,b₁ st b₂ tolerates b₃

proof end;

theorem Th150: :: FUNCT_2:150

canceled;

theorem Th151: :: FUNCT_2:151

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ tolerates b₅ & b₄ tolerates b₅ holds
b₃ tolerates b₄

proof end;

theorem Th152: :: FUNCT_2:152

for b₁ being set
for b₂, b₃ being PartFunc of b₁,b₁
for b₄ being Function of b₁,b₁ st b₂ tolerates b₄ & b₃ tolerates b₄ holds
b₂ tolerates b₃

proof end;

theorem Th153: :: FUNCT_2:153

canceled;

theorem Th154: :: FUNCT_2:154

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ tolerates b₄ holds
ex b₅ being Function of b₁,b₂ st
( b₃ tolerates b₅ & b₄ tolerates b₅ )

proof end;

theorem Th155: :: FUNCT_2:155

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ tolerates b₄ holds
b₄ in TotFuncs b₃

proof end;

theorem Th156: :: FUNCT_2:156

for b₁ being set
for b₂ being PartFunc of b₁,b₁
for b₃ being Function of b₁,b₁ st b₂ tolerates b₃ holds
b₃ in TotFuncs b₂

proof end;

theorem Th157: :: FUNCT_2:157

canceled;

theorem Th158: :: FUNCT_2:158

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂
for b₄ being set st b₄ in TotFuncs b₃ holds
b₄ is Function of b₁,b₂

proof end;

theorem Th159: :: FUNCT_2:159

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ holds TotFuncs b₃ c= Funcs b₁,b₂

proof end;

theorem Th160: :: FUNCT_2:160

for b₁, b₂ being set holds TotFuncs <:{} ,b₁,b₂:> = Funcs b₁,b₂

proof end;

theorem Th161: :: FUNCT_2:161

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
TotFuncs <:b₃,b₁,b₂:> = {b₃}

proof end;

theorem Th162: :: FUNCT_2:162

for b₁ being set
for b₂ being Function of b₁,b₁ holds TotFuncs <:b₂,b₁,b₁:> = {b₂}

proof end;

theorem Th163: :: FUNCT_2:163

canceled;

theorem Th164: :: FUNCT_2:164

for b₁, b₂ being set
for b₃ being PartFunc of b₁,{b₂}
for b₄ being Function of b₁,{b₂} holds TotFuncs b₃ = {b₄}

proof end;

theorem Th165: :: FUNCT_2:165

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st b₄ c= b₃ holds
TotFuncs b₃ c= TotFuncs b₄

proof end;

theorem Th166: :: FUNCT_2:166

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st dom b₄ c= dom b₃ & TotFuncs b₃ c= TotFuncs b₄ holds
b₄ c= b₃

proof end;

theorem Th167: :: FUNCT_2:167

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st TotFuncs b₃ c= TotFuncs b₄ & ( for b₅ being set holds b₂ <> {b₅} ) holds
b₄ c= b₃

proof end;

theorem Th168: :: FUNCT_2:168

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st ( for b₅ being set holds b₂ <> {b₅} ) & TotFuncs b₃ = TotFuncs b₄ holds
b₃ = b₄

proof end;

registration

let c₁, c₂ be non empty set ;
cluster -> non empty total Relation of a₁,a₂;
coherence by Def1, RELAT_1:60;

end;

definition

let c₁, c₂, c₃ be set ;
func c₁,c₂ :-> c₃ -> Function of [:{a₁},{a₂}:],{a₃} means :: FUNCT_2:def 5
verum;
existence ;
uniqueness by Th66;

end;

:: deftheorem Def5 defines :-> FUNCT_2:def 5 :

scheme :: FUNCT_2:sch 10
s10{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₂(), F₅( set ) -> Element of F₂() } :

ex b₁ being Function of F₁(),F₂() st
( b₁ . F₃() = F₄() & ( for b₂ being Element of F₁() st b₂ <> F₃() holds
b₁ . b₂ = F₅(b₂) ) )

proof end;

scheme :: FUNCT_2:sch 11
s11{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₂(), F₆() -> Element of F₂(), F₇( set ) -> Element of F₂() } :

ex b₁ being Function of F₁(),F₂() st
( b₁ . F₃() = F₅() & b₁ . F₄() = F₆() & ( for b₂ being Element of F₁() st b₂ <> F₃() & b₂ <> F₄() holds
b₁ . b₂ = F₇(b₂) ) )

provided

E43: F₃() <> F₄()

proof end;

theorem Th169: :: FUNCT_2:169

for b₁, b₂ being set
for b₃ being Function st b₃ in Funcs b₁,b₂ holds
( dom b₃ = b₁ & rng b₃ c= b₂ )

proof end;

scheme :: FUNCT_2:sch 12
s12{ F₁() -> non empty set , F₂() -> set , F₃( set ) -> set } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being Element of F₁() holds b₁ . b₂ = F₃(b₂)

provided

E43: for b₁ being Element of F₁() holds F₃(b₁) in F₂()

proof end;

scheme :: FUNCT_2:sch 13
s13{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> set } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being Element of F₁() holds b₁ . b₂ = F₃(b₂)

provided

E43: for b₁ being Element of F₁() holds F₃(b₁) is Element of F₂()

proof end;

scheme :: FUNCT_2:sch 14
s14{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex b₁ being Function of F₁(),F₂() st
for b₂ being Element of F₁() holds P₁[b₂,b₁ . b₂]

provided

E43: for b₁ being Element of F₁() ex b₂ being Element of F₂() st P₁[b₁,b₂]

proof end;