:: by Jaros{\l}aw Kotowicz

::

:: Received May 31, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th1: :: PARTFUN2:1

for D, C being non empty set

for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds

f /. c = g /. c ) holds

f = g

for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds

f /. c = g /. c ) holds

f = g

proof end;

theorem Th2: :: PARTFUN2:2

for y being set

for D, C being non empty set

for f being PartFunc of C,D holds

( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

for D, C being non empty set

for f being PartFunc of C,D holds

( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

proof end;

theorem Th3: :: PARTFUN2:3

for D, E, C being non empty set

for f being PartFunc of C,D

for s being PartFunc of D,E

for h being PartFunc of C,E holds

( h = s * f iff ( ( for c being Element of C holds

( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds

h /. c = s /. (f /. c) ) ) )

for f being PartFunc of C,D

for s being PartFunc of D,E

for h being PartFunc of C,E holds

( h = s * f iff ( ( for c being Element of C holds

( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds

h /. c = s /. (f /. c) ) ) )

proof end;

theorem Th4: :: PARTFUN2:4

for C, D, E being non empty set

for c being Element of C

for f being PartFunc of C,D

for s being PartFunc of D,E st c in dom f & f /. c in dom s holds

(s * f) /. c = s /. (f /. c)

for c being Element of C

for f being PartFunc of C,D

for s being PartFunc of D,E st c in dom f & f /. c in dom s holds

(s * f) /. c = s /. (f /. c)

proof end;

theorem :: PARTFUN2:5

for C, D, E being non empty set

for c being Element of C

for f being PartFunc of C,D

for s being PartFunc of D,E st rng f c= dom s & c in dom f holds

(s * f) /. c = s /. (f /. c)

for c being Element of C

for f being PartFunc of C,D

for s being PartFunc of D,E st rng f c= dom s & c in dom f holds

(s * f) /. c = s /. (f /. c)

proof end;

definition

let D be non empty set ;

let SD be Subset of D;

:: original: id

redefine func id SD -> PartFunc of D,D;

coherence

id SD is PartFunc of D,D

end;
let SD be Subset of D;

:: original: id

redefine func id SD -> PartFunc of D,D;

coherence

id SD is PartFunc of D,D

proof end;

theorem Th6: :: PARTFUN2:6

for D being non empty set

for SD being Subset of D

for F being PartFunc of D,D holds

( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds

F /. d = d ) ) )

for SD being Subset of D

for F being PartFunc of D,D holds

( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds

F /. d = d ) ) )

proof end;

theorem :: PARTFUN2:7

for D being non empty set

for SD being Subset of D

for d being Element of D

for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

for SD being Subset of D

for d being Element of D

for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

proof end;

theorem :: PARTFUN2:8

for D being non empty set

for SD being Subset of D

for d being Element of D

for F being PartFunc of D,D holds

( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )

for SD being Subset of D

for d being Element of D

for F being PartFunc of D,D holds

( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )

proof end;

theorem :: PARTFUN2:9

for D, C being non empty set

for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds

c1 = c2 ) holds

f is one-to-one

for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds

c1 = c2 ) holds

f is one-to-one

proof end;

theorem :: PARTFUN2:10

for x, y being set

for C, D being non empty set

for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds

x = y

for C, D being non empty set

for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds

x = y

proof end;

definition

let X, Y be set ;

let f be one-to-one PartFunc of X,Y;

:: original: "

redefine func f " -> PartFunc of Y,X;

coherence

f " is PartFunc of Y,X by PARTFUN1:9;

end;
let f be one-to-one PartFunc of X,Y;

:: original: "

redefine func f " -> PartFunc of Y,X;

coherence

f " is PartFunc of Y,X by PARTFUN1:9;

theorem Th11: :: PARTFUN2:11

for C, D being non empty set

for f being one-to-one PartFunc of C,D

for g being PartFunc of D,C holds

( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

for f being one-to-one PartFunc of C,D

for g being PartFunc of D,C holds

( g = f " iff ( dom g = rng f & ( for d being Element of D

for c being Element of C holds

( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

proof end;

theorem :: PARTFUN2:12

for C, D being non empty set

for c being Element of C

for f being one-to-one PartFunc of C,D st c in dom f holds

( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )

for c being Element of C

for f being one-to-one PartFunc of C,D st c in dom f holds

( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )

proof end;

theorem :: PARTFUN2:13

for C, D being non empty set

for d being Element of D

for f being one-to-one PartFunc of C,D st d in rng f holds

( d = f /. ((f ") /. d) & d = (f * (f ")) /. d )

for d being Element of D

for f being one-to-one PartFunc of C,D st d in rng f holds

( d = f /. ((f ") /. d) & d = (f * (f ")) /. d )

proof end;

theorem :: PARTFUN2:14

for C, D being non empty set

for f being PartFunc of C,D

for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C

for d being Element of D st c in dom f & d in dom t holds

( f /. c = d iff t /. d = c ) ) holds

t = f "

for f being PartFunc of C,D

for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C

for d being Element of D st c in dom f & d in dom t holds

( f /. c = d iff t /. d = c ) ) holds

t = f "

proof end;

theorem Th15: :: PARTFUN2:15

for X being set

for D, C being non empty set

for g, f being PartFunc of C,D holds

( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds

g /. c = f /. c ) ) )

for D, C being non empty set

for g, f being PartFunc of C,D holds

( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds

g /. c = f /. c ) ) )

proof end;

theorem Th16: :: PARTFUN2:16

for X being set

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in (dom f) /\ X holds

(f | X) /. c = f /. c

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in (dom f) /\ X holds

(f | X) /. c = f /. c

proof end;

theorem :: PARTFUN2:17

for X being set

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in dom f & c in X holds

(f | X) /. c = f /. c

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in dom f & c in X holds

(f | X) /. c = f /. c

proof end;

theorem :: PARTFUN2:18

for X being set

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in dom f & c in X holds

f /. c in rng (f | X)

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in dom f & c in X holds

f /. c in rng (f | X)

proof end;

definition

let C, D be non empty set ;

let X be set ;

let f be PartFunc of C,D;

:: original: |`

redefine func X |` f -> PartFunc of C,D;

coherence

X |` f is PartFunc of C,D by PARTFUN1:13;

end;
let X be set ;

let f be PartFunc of C,D;

:: original: |`

redefine func X |` f -> PartFunc of C,D;

coherence

X |` f is PartFunc of C,D by PARTFUN1:13;

theorem Th19: :: PARTFUN2:19

for X being set

for D, C being non empty set

for g, f being PartFunc of C,D holds

( g = X |` f iff ( ( for c being Element of C holds

( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds

g /. c = f /. c ) ) )

for D, C being non empty set

for g, f being PartFunc of C,D holds

( g = X |` f iff ( ( for c being Element of C holds

( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds

g /. c = f /. c ) ) )

proof end;

theorem :: PARTFUN2:20

theorem :: PARTFUN2:21

theorem Th22: :: PARTFUN2:22

for X being set

for D, C being non empty set

for SD being Subset of D

for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

for D, C being non empty set

for SD being Subset of D

for f being PartFunc of C,D holds

( SD = f .: X iff for d being Element of D holds

( d in SD iff ex c being Element of C st

( c in dom f & c in X & d = f /. c ) ) )

proof end;

theorem :: PARTFUN2:23

theorem :: PARTFUN2:24

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st c in dom f holds

Im (f,c) = {(f /. c)}

for c being Element of C

for f being PartFunc of C,D st c in dom f holds

Im (f,c) = {(f /. c)}

proof end;

theorem :: PARTFUN2:25

for C, D being non empty set

for c1, c2 being Element of C

for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds

f .: {c1,c2} = {(f /. c1),(f /. c2)}

for c1, c2 being Element of C

for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds

f .: {c1,c2} = {(f /. c1),(f /. c2)}

proof end;

theorem Th26: :: PARTFUN2:26

for X being set

for D, C being non empty set

for SC being Subset of C

for f being PartFunc of C,D holds

( SC = f " X iff for c being Element of C holds

( c in SC iff ( c in dom f & f /. c in X ) ) )

for D, C being non empty set

for SC being Subset of C

for f being PartFunc of C,D holds

( SC = f " X iff for c being Element of C holds

( c in SC iff ( c in dom f & f /. c in X ) ) )

proof end;

theorem :: PARTFUN2:27

for D, C being non empty set

for f being PartFunc of C,D ex g being Function of C,D st

for c being Element of C st c in dom f holds

g . c = f /. c

for f being PartFunc of C,D ex g being Function of C,D st

for c being Element of C st c in dom f holds

g . c = f /. c

proof end;

theorem :: PARTFUN2:28

for D, C being non empty set

for f, g being PartFunc of C,D holds

( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds

f /. c = g /. c )

for f, g being PartFunc of C,D holds

( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds

f /. c = g /. c )

proof end;

scheme :: PARTFUN2:sch 1

PartFuncExD{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set ] } :

PartFuncExD{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for d being Element of F_{1}() holds

( d in dom f iff ex c being Element of F_{2}() st P_{1}[d,c] ) ) & ( for d being Element of F_{1}() st d in dom f holds

P_{1}[d,f /. d] ) )

( ( for d being Element of F

( d in dom f iff ex c being Element of F

P

proof end;

scheme :: PARTFUN2:sch 2

LambdaPFD{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), P_{1}[ set ] } :

LambdaPFD{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for d being Element of F_{1}() holds

( d in dom f iff P_{1}[d] ) ) & ( for d being Element of F_{1}() st d in dom f holds

f /. d = F_{3}(d) ) )

( ( for d being Element of F

( d in dom f iff P

f /. d = F

proof end;

scheme :: PARTFUN2:sch 3

UnPartFuncD{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> set , F_{4}( set ) -> Element of F_{2}() } :

UnPartFuncD{ F

for f, g being PartFunc of F_{1}(),F_{2}() st dom f = F_{3}() & ( for c being Element of F_{1}() st c in dom f holds

f /. c = F_{4}(c) ) & dom g = F_{3}() & ( for c being Element of F_{1}() st c in dom g holds

g /. c = F_{4}(c) ) holds

f = g

f /. c = F

g /. c = F

f = g

proof end;

definition

let C, D be non empty set ;

let SC be Subset of C;

let d be Element of D;

:: original: -->

redefine func SC --> d -> PartFunc of C,D;

coherence

SC --> d is PartFunc of C,D

end;
let SC be Subset of C;

let d be Element of D;

:: original: -->

redefine func SC --> d -> PartFunc of C,D;

coherence

SC --> d is PartFunc of C,D

proof end;

theorem Th29: :: PARTFUN2:29

for C, D being non empty set

for SC being Subset of C

for c being Element of C

for d being Element of D st c in SC holds

(SC --> d) /. c = d

for SC being Subset of C

for c being Element of C

for d being Element of D st c in SC holds

(SC --> d) /. c = d

proof end;

theorem :: PARTFUN2:30

for D, C being non empty set

for d being Element of D

for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds

f /. c = d ) holds

f = (dom f) --> d

for d being Element of D

for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds

f /. c = d ) holds

f = (dom f) --> d

proof end;

theorem :: PARTFUN2:31

for E, C, D being non empty set

for SE being Subset of E

for c being Element of C

for f being PartFunc of C,D st c in dom f holds

f * (SE --> c) = SE --> (f /. c)

for SE being Subset of E

for c being Element of C

for f being PartFunc of C,D st c in dom f holds

f * (SE --> c) = SE --> (f /. c)

proof end;

theorem :: PARTFUN2:33

for C, D being non empty set

for SC being Subset of C

for d being Element of D st SC --> d is total holds

SC <> {}

for SC being Subset of C

for d being Element of D st SC --> d is total holds

SC <> {}

proof end;

theorem :: PARTFUN2:34

for D, C being non empty set

for SC being Subset of C

for d being Element of D holds

( SC --> d is total iff SC = C )

for SC being Subset of C

for d being Element of D holds

( SC --> d is total iff SC = C )

proof end;

definition

let C, D be non empty set ;

let f be PartFunc of C,D;

( f is constant iff ex d being Element of D st

for c being Element of C st c in dom f holds

f . c = d )

end;
let f be PartFunc of C,D;

:: original: constant

redefine attr f is constant means :: PARTFUN2:def 1

ex d being Element of D st

for c being Element of C st c in dom f holds

f . c = d;

compatibility redefine attr f is constant means :: PARTFUN2:def 1

ex d being Element of D st

for c being Element of C st c in dom f holds

f . c = d;

( f is constant iff ex d being Element of D st

for c being Element of C st c in dom f holds

f . c = d )

proof end;

:: deftheorem defines constant PARTFUN2:def 1 :

for C, D being non empty set

for f being PartFunc of C,D holds

( f is constant iff ex d being Element of D st

for c being Element of C st c in dom f holds

f . c = d );

for C, D being non empty set

for f being PartFunc of C,D holds

( f is constant iff ex d being Element of D st

for c being Element of C st c in dom f holds

f . c = d );

theorem Th35: :: PARTFUN2:35

for X being set

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff ex d being Element of D st

for c being Element of C st c in X /\ (dom f) holds

f /. c = d )

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff ex d being Element of D st

for c being Element of C st c in X /\ (dom f) holds

f /. c = d )

proof end;

theorem :: PARTFUN2:36

for X being set

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds

f /. c1 = f /. c2 )

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds

f /. c1 = f /. c2 )

proof end;

theorem :: PARTFUN2:37

for X being set

for C, D being non empty set

for f being PartFunc of C,D st X meets dom f holds

( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

for C, D being non empty set

for f being PartFunc of C,D st X meets dom f holds

( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

proof end;

theorem :: PARTFUN2:38

for X, Y being set

for C, D being non empty set

for f being PartFunc of C,D st f | X is V8() & Y c= X holds

f | Y is V8()

for C, D being non empty set

for f being PartFunc of C,D st f | X is V8() & Y c= X holds

f | Y is V8()

proof end;

theorem Th39: :: PARTFUN2:39

for X being set

for C, D being non empty set

for f being PartFunc of C,D st X misses dom f holds

f | X is V8()

for C, D being non empty set

for f being PartFunc of C,D st X misses dom f holds

f | X is V8()

proof end;

theorem :: PARTFUN2:40

for C, D being non empty set

for SC being Subset of C

for d being Element of D

for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds

f | SC is V8()

for SC being Subset of C

for d being Element of D

for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds

f | SC is V8()

proof end;

theorem :: PARTFUN2:42

for X, Y being set

for C, D being non empty set

for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds

f | (X \/ Y) is V8()

for C, D being non empty set

for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds

f | (X \/ Y) is V8()

proof end;

theorem :: PARTFUN2:43

for Y, X being set

for C, D being non empty set

for f being PartFunc of C,D st f | Y is V8() holds

(f | X) | Y is V8()

for C, D being non empty set

for f being PartFunc of C,D st f | Y is V8() holds

(f | X) | Y is V8()

proof end;

theorem :: PARTFUN2:44

for C, D being non empty set

for SC being Subset of C

for d being Element of D holds (SC --> d) | SC is V8()

for SC being Subset of C

for d being Element of D holds (SC --> d) | SC is V8()

proof end;

::

:: OF PARTIAL FUNCTION FROM A DOMAIN TO A DOMAIN

::

:: OF PARTIAL FUNCTION FROM A DOMAIN TO A DOMAIN

::

theorem :: PARTFUN2:45

for D, C being non empty set

for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds

f /. c = g /. c ) holds

f c= g

for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds

f /. c = g /. c ) holds

f c= g

proof end;

theorem Th46: :: PARTFUN2:46

for C, D being non empty set

for c being Element of C

for d being Element of D

for f being PartFunc of C,D holds

( ( c in dom f & d = f /. c ) iff [c,d] in f )

for c being Element of C

for d being Element of D

for f being PartFunc of C,D holds

( ( c in dom f & d = f /. c ) iff [c,d] in f )

proof end;

theorem :: PARTFUN2:47

for C, D, E being non empty set

for c being Element of C

for e being Element of E

for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

for c being Element of C

for e being Element of E

for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

proof end;

theorem :: PARTFUN2:48

for C, D being non empty set

for c being Element of C

for d being Element of D

for f being PartFunc of C,D st f = {[c,d]} holds

f /. c = d

for c being Element of C

for d being Element of D

for f being PartFunc of C,D st f = {[c,d]} holds

f /. c = d

proof end;

theorem :: PARTFUN2:49

for C, D being non empty set

for c being Element of C

for f being PartFunc of C,D st dom f = {c} holds

f = {[c,(f /. c)]}

for c being Element of C

for f being PartFunc of C,D st dom f = {c} holds

f = {[c,(f /. c)]}

proof end;

theorem :: PARTFUN2:50

for C, D being non empty set

for c being Element of C

for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds

( f1 /. c = f /. c & f1 /. c = g /. c )

for c being Element of C

for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds

( f1 /. c = f /. c & f1 /. c = g /. c )

proof end;

theorem :: PARTFUN2:51

for C, D being non empty set

for c being Element of C

for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds

f1 /. c = f /. c

for c being Element of C

for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds

f1 /. c = f /. c

proof end;

theorem :: PARTFUN2:52

for C, D being non empty set

for c being Element of C

for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds

f1 /. c = g /. c

for c being Element of C

for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds

f1 /. c = g /. c

proof end;

theorem :: PARTFUN2:53

for C, D being non empty set

for c being Element of C

for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds

f1 /. c = g /. c

for c being Element of C

for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds

f1 /. c = g /. c

proof end;

theorem :: PARTFUN2:54

for C, D being non empty set

for SC being Subset of C

for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )

for SC being Subset of C

for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )

proof end;

theorem :: PARTFUN2:55

for C, D being non empty set

for SD being Subset of D

for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

for SD being Subset of D

for c being Element of C

for f being PartFunc of C,D holds

( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )

proof end;

theorem :: PARTFUN2:56

for C, D being non empty set

for SD being Subset of D

for c being Element of C

for f being PartFunc of C,D holds

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

for SD being Subset of D

for c being Element of C

for f being PartFunc of C,D holds

( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

proof end;

theorem Th57: :: PARTFUN2:57

for X being set

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff ex d being Element of D st

for c being Element of C st c in X /\ (dom f) holds

f . c = d )

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff ex d being Element of D st

for c being Element of C st c in X /\ (dom f) holds

f . c = d )

proof end;

theorem :: PARTFUN2:58

for X being set

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds

f . c1 = f . c2 )

for D, C being non empty set

for f being PartFunc of C,D holds

( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds

f . c1 = f . c2 )

proof end;

theorem :: PARTFUN2:59

for X being set

for D, C being non empty set

for d being Element of D

for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

for D, C being non empty set

for d being Element of D

for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

proof end;

theorem :: PARTFUN2:60

for C, D being non empty set

for c being Element of C

for d being Element of D

for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

for c being Element of C

for d being Element of D

for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

proof end;

theorem :: PARTFUN2:61

for Y being set

for f, g being b_{1} -valued Function st f c= g holds

for x being set st x in dom f holds

f /. x = g /. x

for f, g being b

for x being set st x in dom f holds

f /. x = g /. x

proof end;

:: PARTIAL FUNCTION CONSTANT ON SET

::