:: Partial Functions from a Domain to a Domain :: by Jaros{\l}aw Kotowicz :: :: Received May 31, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users
for D being non emptyset 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 X being set for D, C being non emptyset for g, f being PartFunc of C,D holds ( g = X |` f iff ( ( for c being Element of C holds ( c indom g iff ( c indom f & f /. c in X ) ) ) & ( for c being Element of C st c indom g holds g /. c = f /. c ) ) )
for X being set for D, C being non emptyset 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 indom f & c in X & d = f /. c ) ) )
for X being set for D, C being non emptyset 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 indom f & f /. c in X ) ) )
ex f being PartFunc of F1(),F2() st ( ( for d being Element of F1() holds ( d indom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d indom f holds P1[d,f /. d] ) )
ex f being PartFunc of F1(),F2() st ( ( for d being Element of F1() holds ( d indom f iff P1[d] ) ) & ( for d being Element of F1() st d indom f holds f /. d = F3(d) ) )
for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c indom f holds f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c indom g holds g /. c = F4(c) ) holds f = g
for X being set for D, C being non emptyset 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 X being set for D, C being non emptyset 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 X being set for D, C being non emptyset 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 X being set for D, C being non emptyset 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 )
:: PARTIAL FUNCTION CONSTANT ON SET
::