:: PARTFUN2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: PARTFUN2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: PARTFUN2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: PARTFUN2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: PARTFUN2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: PARTFUN2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) ) ) )
proof end;

theorem :: PARTFUN2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: PARTFUN2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: PARTFUN2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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
proof end;
end;

theorem :: PARTFUN2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: PARTFUN2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: PARTFUN2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: PARTFUN2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
cluster {} -> one-to-one ;
coherence
{} is one-to-one
;
end;

registration
let X, Y be set ;
cluster one-to-one Relation of X,Y;
existence
ex b1 being PartFunc of X,Y st b1 is one-to-one
proof end;
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:39;
end;

theorem Th18: :: PARTFUN2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) ) ) )
proof end;

theorem :: PARTFUN2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 "
proof end;

theorem :: PARTFUN2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th32: :: PARTFUN2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: PARTFUN2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: PARTFUN2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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:46;
end;

theorem Th37: :: PARTFUN2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: PARTFUN2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D holds
( c in dom (X | f) iff ( c in dom f & f /. c in X ) ) by Th37;

theorem :: PARTFUN2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 (X | f) holds
(X | f) /. c = f /. c by Th37;

theorem Th40: :: PARTFUN2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: PARTFUN2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C, D being non empty set
for d being Element of D
for f being PartFunc of C,D holds
( d in f .: X iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) by Th40;

theorem :: PARTFUN2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
f .: {c} = {(f /. c)}
proof end;

theorem :: PARTFUN2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem Th44: :: PARTFUN2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: PARTFUN2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

scheme :: PARTFUN2:sch 1
PartFuncExD{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )
proof end;

scheme :: PARTFUN2:sch 2
LambdaPFD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f /. d = F3(d) ) )
proof end;

scheme :: PARTFUN2:sch 3
UnPartFuncD{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4( set ) -> Element of F2() } :
for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c in dom f holds
f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds
g /. c = F4(c) ) holds
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
proof end;
end;

theorem Th48: :: PARTFUN2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: PARTFUN2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for SC being Subset of C holds
( id SC is total iff SC = C )
proof end;

theorem :: PARTFUN2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 <> {}
proof end;

theorem :: PARTFUN2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let C, D be non empty set ;
let f be PartFunc of C,D;
let X be set ;
canceled;
canceled;
pred f is_constant_on X means :Def3: :: PARTFUN2:def 3
ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d;
end;

:: deftheorem PARTFUN2:def 1 :
canceled;

:: deftheorem PARTFUN2:def 2 :
canceled;

:: deftheorem Def3 defines is_constant_on PARTFUN2:def 3 :
for C, D being non empty set
for f being PartFunc of C,D
for X being set holds
( f is_constant_on X iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d );

theorem :: PARTFUN2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARTFUN2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f is_constant_on X 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:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 is_constant_on X iff ex d being Element of D st rng (f | X) = {d} )
proof end;

theorem :: PARTFUN2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f is_constant_on X & Y c= X holds
f is_constant_on Y
proof end;

theorem Th58: :: PARTFUN2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 is_constant_on X
proof end;

theorem :: PARTFUN2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 is_constant_on SC
proof end;

theorem :: PARTFUN2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for C, D being non empty set
for f being PartFunc of C,D holds f is_constant_on {x}
proof end;

theorem :: PARTFUN2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f is_constant_on X & f is_constant_on Y & X /\ Y meets dom f holds
f is_constant_on X \/ Y
proof end;

theorem :: PARTFUN2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set
for C, D being non empty set
for f being PartFunc of C,D st f is_constant_on Y holds
f | X is_constant_on Y
proof end;

theorem :: PARTFUN2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for SC being Subset of C
for d being Element of D holds SC --> d is_constant_on SC
proof end;

theorem :: PARTFUN2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C being non empty set
for f, g being PartFunc of C,D holds
( f c= g iff ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) )
proof end;

theorem Th65: :: PARTFUN2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]}
proof end;

theorem :: PARTFUN2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PARTFUN2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th76: :: PARTFUN2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f is_constant_on X 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:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f is_constant_on X 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:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PARTFUN2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;