:: PARTFUN2 semantic presentation

theorem Th1: :: PARTFUN2:1
canceled;

theorem Th2: :: PARTFUN2:2
canceled;

theorem Th3: :: PARTFUN2:3
for b1, b2 being non empty set
for b3, b4 being PartFunc of b2,b1 st dom b3 = dom b4 & ( for b5 being Element of b2 st b5 in dom b3 holds
b3 /. b5 = b4 /. b5 ) holds
b3 = b4
proof end;

theorem Th4: :: PARTFUN2:4
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b3,b2 holds
( b1 in rng b4 iff ex b5 being Element of b3 st
( b5 in dom b4 & b1 = b4 /. b5 ) )
proof end;

theorem Th5: :: PARTFUN2:5
canceled;

theorem Th6: :: PARTFUN2:6
for b1, b2, b3 being non empty set
for b4 being PartFunc of b3,b1
for b5 being PartFunc of b1,b2
for b6 being PartFunc of b3,b2 holds
( b6 = b5 * b4 iff ( ( for b7 being Element of b3 holds
( b7 in dom b6 iff ( b7 in dom b4 & b4 /. b7 in dom b5 ) ) ) & ( for b7 being Element of b3 st b7 in dom b6 holds
b6 /. b7 = b5 /. (b4 /. b7) ) ) )
proof end;

theorem Th7: :: PARTFUN2:7
canceled;

theorem Th8: :: PARTFUN2:8
canceled;

theorem Th9: :: PARTFUN2:9
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being PartFunc of b1,b2
for b6 being PartFunc of b2,b3 st b4 in dom b5 & b5 /. b4 in dom b6 holds
(b6 * b5) /. b4 = b6 /. (b5 /. b4)
proof end;

theorem Th10: :: PARTFUN2:10
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being PartFunc of b1,b2
for b6 being PartFunc of b2,b3 st rng b5 c= dom b6 & b4 in dom b5 holds
(b6 * b5) /. b4 = b6 /. (b5 /. b4)
proof end;

definition
let c1 be non empty set ;
let c2 be Subset of c1;
redefine func id as id c2 -> PartFunc of a1,a1;
coherence
id c2 is PartFunc of c1,c1
proof end;
end;

theorem Th11: :: PARTFUN2:11
canceled;

theorem Th12: :: PARTFUN2:12
for b1 being non empty set
for b2 being Subset of b1
for b3 being PartFunc of b1,b1 holds
( b3 = id b2 iff ( dom b3 = b2 & ( for b4 being Element of b1 st b4 in b2 holds
b3 /. b4 = b4 ) ) )
proof end;

theorem Th13: :: PARTFUN2:13
canceled;

theorem Th14: :: PARTFUN2:14
for b1 being non empty set
for b2 being Subset of b1
for b3 being Element of b1
for b4 being PartFunc of b1,b1 st b3 in (dom b4) /\ b2 holds
b4 /. b3 = (b4 * (id b2)) /. b3
proof end;

theorem Th15: :: PARTFUN2:15
for b1 being non empty set
for b2 being Subset of b1
for b3 being Element of b1
for b4 being PartFunc of b1,b1 holds
( b3 in dom ((id b2) * b4) iff ( b3 in dom b4 & b4 /. b3 in b2 ) )
proof end;

theorem Th16: :: PARTFUN2:16
for b1, b2 being non empty set
for b3 being PartFunc of b2,b1 st ( for b4, b5 being Element of b2 st b4 in dom b3 & b5 in dom b3 & b3 /. b4 = b3 /. b5 holds
b4 = b5 ) holds
b3 is one-to-one
proof end;

theorem Th17: :: PARTFUN2:17
for b1, b2 being set
for b3, b4 being non empty set
for b5 being PartFunc of b3,b4 st b5 is one-to-one & b1 in dom b5 & b2 in dom b5 & b5 /. b1 = b5 /. b2 holds
b1 = b2
proof end;

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

registration
let c1, c2 be set ;
cluster one-to-one Relation of a1,a2;
existence
ex b1 being PartFunc of c1,c2 st b1 is one-to-one
proof end;
end;

definition
let c1, c2 be set ;
let c3 be one-to-one PartFunc of c1,c2;
redefine func " as c3 " -> PartFunc of a2,a1;
coherence
c3 " is PartFunc of c2,c1 by PARTFUN1:39;
end;

theorem Th18: :: PARTFUN2:18
for b1, b2 being non empty set
for b3 being one-to-one PartFunc of b1,b2
for b4 being PartFunc of b2,b1 holds
( b4 = b3 " iff ( dom b4 = rng b3 & ( for b5 being Element of b2
for b6 being Element of b1 holds
( b5 in rng b3 & b6 = b4 /. b5 iff ( b6 in dom b3 & b5 = b3 /. b6 ) ) ) ) )
proof end;

theorem Th19: :: PARTFUN2:19
canceled;

theorem Th20: :: PARTFUN2:20
canceled;

theorem Th21: :: PARTFUN2:21
canceled;

theorem Th22: :: PARTFUN2:22
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being one-to-one PartFunc of b1,b2 st b3 in dom b4 holds
( b3 = (b4 " ) /. (b4 /. b3) & b3 = ((b4 " ) * b4) /. b3 )
proof end;

theorem Th23: :: PARTFUN2:23
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being one-to-one PartFunc of b1,b2 st b3 in rng b4 holds
( b3 = b4 /. ((b4 " ) /. b3) & b3 = (b4 * (b4 " )) /. b3 )
proof end;

theorem Th24: :: PARTFUN2:24
for b1, b2 being non empty set
for b3 being PartFunc of b1,b2
for b4 being PartFunc of b2,b1 st b3 is one-to-one & dom b3 = rng b4 & rng b3 = dom b4 & ( for b5 being Element of b1
for b6 being Element of b2 st b5 in dom b3 & b6 in dom b4 holds
( b3 /. b5 = b6 iff b4 /. b6 = b5 ) ) holds
b4 = b3 "
proof end;

theorem Th25: :: PARTFUN2:25
canceled;

theorem Th26: :: PARTFUN2:26
canceled;

theorem Th27: :: PARTFUN2:27
canceled;

theorem Th28: :: PARTFUN2:28
canceled;

theorem Th29: :: PARTFUN2:29
canceled;

theorem Th30: :: PARTFUN2:30
canceled;

theorem Th31: :: PARTFUN2:31
canceled;

theorem Th32: :: PARTFUN2:32
for b1 being set
for b2, b3 being non empty set
for b4, b5 being PartFunc of b3,b2 holds
( b4 = b5 | b1 iff ( dom b4 = (dom b5) /\ b1 & ( for b6 being Element of b3 st b6 in dom b4 holds
b4 /. b6 = b5 /. b6 ) ) )
proof end;

theorem Th33: :: PARTFUN2:33
canceled;

theorem Th34: :: PARTFUN2:34
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b2
for b5 being PartFunc of b2,b3 st b4 in (dom b5) /\ b1 holds
(b5 | b1) /. b4 = b5 /. b4
proof end;

theorem Th35: :: PARTFUN2:35
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b2
for b5 being PartFunc of b2,b3 st b4 in dom b5 & b4 in b1 holds
(b5 | b1) /. b4 = b5 /. b4
proof end;

theorem Th36: :: PARTFUN2:36
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b2
for b5 being PartFunc of b2,b3 st b4 in dom b5 & b4 in b1 holds
b5 /. b4 in rng (b5 | b1)
proof end;

definition
let c1, c2 be non empty set ;
let c3 be set ;
let c4 be PartFunc of c1,c2;
redefine func | as c3 | c4 -> PartFunc of a1,a2;
coherence
c3 | c4 is PartFunc of c1,c2 by PARTFUN1:46;
end;

theorem Th37: :: PARTFUN2:37
for b1 being set
for b2, b3 being non empty set
for b4, b5 being PartFunc of b3,b2 holds
( b4 = b1 | b5 iff ( ( for b6 being Element of b3 holds
( b6 in dom b4 iff ( b6 in dom b5 & b5 /. b6 in b1 ) ) ) & ( for b6 being Element of b3 st b6 in dom b4 holds
b4 /. b6 = b5 /. b6 ) ) )
proof end;

theorem Th38: :: PARTFUN2:38
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b2
for b5 being PartFunc of b2,b3 holds
( b4 in dom (b1 | b5) iff ( b4 in dom b5 & b5 /. b4 in b1 ) ) by Th37;

theorem Th39: :: PARTFUN2:39
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b2
for b5 being PartFunc of b2,b3 st b4 in dom (b1 | b5) holds
(b1 | b5) /. b4 = b5 /. b4 by Th37;

theorem Th40: :: PARTFUN2:40
for b1 being set
for b2, b3 being non empty set
for b4 being Subset of b2
for b5 being PartFunc of b3,b2 holds
( b4 = b5 .: b1 iff for b6 being Element of b2 holds
( b6 in b4 iff ex b7 being Element of b3 st
( b7 in dom b5 & b7 in b1 & b6 = b5 /. b7 ) ) )
proof end;

theorem Th41: :: PARTFUN2:41
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b3
for b5 being PartFunc of b2,b3 holds
( b4 in b5 .: b1 iff ex b6 being Element of b2 st
( b6 in dom b5 & b6 in b1 & b4 = b5 /. b6 ) ) by Th40;

theorem Th42: :: PARTFUN2:42
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being PartFunc of b1,b2 st b3 in dom b4 holds
b4 .: {b3} = {(b4 /. b3)}
proof end;

theorem Th43: :: PARTFUN2:43
for b1, b2 being non empty set
for b3, b4 being Element of b1
for b5 being PartFunc of b1,b2 st b3 in dom b5 & b4 in dom b5 holds
b5 .: {b3,b4} = {(b5 /. b3),(b5 /. b4)}
proof end;

theorem Th44: :: PARTFUN2:44
for b1 being set
for b2, b3 being non empty set
for b4 being Subset of b3
for b5 being PartFunc of b3,b2 holds
( b4 = b5 " b1 iff for b6 being Element of b3 holds
( b6 in b4 iff ( b6 in dom b5 & b5 /. b6 in b1 ) ) )
proof end;

theorem Th45: :: PARTFUN2:45
canceled;

theorem Th46: :: PARTFUN2:46
for b1, b2 being non empty set
for b3 being PartFunc of b2,b1 ex b4 being Function of b2,b1 st
for b5 being Element of b2 st b5 in dom b3 holds
b4 . b5 = b3 /. b5
proof end;

theorem Th47: :: PARTFUN2:47
for b1, b2 being non empty set
for b3, b4 being PartFunc of b2,b1 holds
( b3 tolerates b4 iff for b5 being Element of b2 st b5 in (dom b3) /\ (dom b4) holds
b3 /. b5 = b4 /. b5 )
proof end;

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

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

scheme :: PARTFUN2:sch 3
s3{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4( set ) -> Element of F2() } :
for b1, b2 being PartFunc of F1(),F2() st dom b1 = F3() & ( for b3 being Element of F1() st b3 in dom b1 holds
b1 /. b3 = F4(b3) ) & dom b2 = F3() & ( for b3 being Element of F1() st b3 in dom b2 holds
b2 /. b3 = F4(b3) ) holds
b1 = b2
proof end;

definition
let c1, c2 be non empty set ;
let c3 be Subset of c1;
let c4 be Element of c2;
redefine func --> as c3 --> c4 -> PartFunc of a1,a2;
coherence
c3 --> c4 is PartFunc of c1,c2
proof end;
end;

theorem Th48: :: PARTFUN2:48
for b1, b2 being non empty set
for b3 being Subset of b1
for b4 being Element of b1
for b5 being Element of b2 st b4 in b3 holds
(b3 --> b5) /. b4 = b5
proof end;

theorem Th49: :: PARTFUN2:49
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being PartFunc of b2,b1 st ( for b5 being Element of b2 st b5 in dom b4 holds
b4 /. b5 = b3 ) holds
b4 = (dom b4) --> b3
proof end;

theorem Th50: :: PARTFUN2:50
for b1, b2, b3 being non empty set
for b4 being Subset of b1
for b5 being Element of b2
for b6 being PartFunc of b2,b3 st b5 in dom b6 holds
b6 * (b4 --> b5) = b4 --> (b6 /. b5)
proof end;

theorem Th51: :: PARTFUN2:51
for b1 being non empty set
for b2 being Subset of b1 holds
( id b2 is total iff b2 = b1 )
proof end;

theorem Th52: :: PARTFUN2:52
for b1, b2 being non empty set
for b3 being Subset of b1
for b4 being Element of b2 st b3 --> b4 is total holds
b3 <> {}
proof end;

theorem Th53: :: PARTFUN2:53
for b1, b2 being non empty set
for b3 being Subset of b2
for b4 being Element of b1 holds
( b3 --> b4 is total iff b3 = b2 )
proof end;

definition
let c1, c2 be non empty set ;
let c3 be PartFunc of c1,c2;
let c4 be set ;
canceled;
canceled;
pred c3 is_constant_on c4 means :Def3: :: PARTFUN2:def 3
ex b1 being Element of a2 st
for b2 being Element of a1 st b2 in a4 /\ (dom a3) holds
a3 /. b2 = b1;
end;

:: deftheorem Def1 PARTFUN2:def 1 :
canceled;

:: deftheorem Def2 PARTFUN2:def 2 :
canceled;

:: deftheorem Def3 defines is_constant_on PARTFUN2:def 3 :
for b1, b2 being non empty set
for b3 being PartFunc of b1,b2
for b4 being set holds
( b3 is_constant_on b4 iff ex b5 being Element of b2 st
for b6 being Element of b1 st b6 in b4 /\ (dom b3) holds
b3 /. b6 = b5 );

theorem Th54: :: PARTFUN2:54
canceled;

theorem Th55: :: PARTFUN2:55
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b3,b2 holds
( b4 is_constant_on b1 iff for b5, b6 being Element of b3 st b5 in b1 /\ (dom b4) & b6 in b1 /\ (dom b4) holds
b4 /. b5 = b4 /. b6 )
proof end;

theorem Th56: :: PARTFUN2:56
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b2,b3 st b1 meets dom b4 holds
( b4 is_constant_on b1 iff ex b5 being Element of b3 st rng (b4 | b1) = {b5} )
proof end;

theorem Th57: :: PARTFUN2:57
for b1, b2 being set
for b3, b4 being non empty set
for b5 being PartFunc of b3,b4 st b5 is_constant_on b1 & b2 c= b1 holds
b5 is_constant_on b2
proof end;

theorem Th58: :: PARTFUN2:58
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b2,b3 st b1 misses dom b4 holds
b4 is_constant_on b1
proof end;

theorem Th59: :: PARTFUN2:59
for b1, b2 being non empty set
for b3 being Subset of b1
for b4 being Element of b2
for b5 being PartFunc of b1,b2 st b5 | b3 = (dom (b5 | b3)) --> b4 holds
b5 is_constant_on b3
proof end;

theorem Th60: :: PARTFUN2:60
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b2,b3 holds b4 is_constant_on {b1}
proof end;

theorem Th61: :: PARTFUN2:61
for b1, b2 being set
for b3, b4 being non empty set
for b5 being PartFunc of b3,b4 st b5 is_constant_on b1 & b5 is_constant_on b2 & b1 /\ b2 meets dom b5 holds
b5 is_constant_on b1 \/ b2
proof end;

theorem Th62: :: PARTFUN2:62
for b1, b2 being set
for b3, b4 being non empty set
for b5 being PartFunc of b3,b4 st b5 is_constant_on b1 holds
b5 | b2 is_constant_on b1
proof end;

theorem Th63: :: PARTFUN2:63
for b1, b2 being non empty set
for b3 being Subset of b1
for b4 being Element of b2 holds b3 --> b4 is_constant_on b3
proof end;

theorem Th64: :: PARTFUN2:64
for b1, b2 being non empty set
for b3, b4 being PartFunc of b2,b1 holds
( b3 c= b4 iff ( dom b3 c= dom b4 & ( for b5 being Element of b2 st b5 in dom b3 holds
b3 /. b5 = b4 /. b5 ) ) )
proof end;

theorem Th65: :: PARTFUN2:65
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being Element of b2
for b5 being PartFunc of b1,b2 holds
( ( b3 in dom b5 & b4 = b5 /. b3 ) iff [b3,b4] in b5 )
proof end;

theorem Th66: :: PARTFUN2:66
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Element of b3
for b6 being PartFunc of b1,b2
for b7 being PartFunc of b2,b3 st [b4,b5] in b7 * b6 holds
( [b4,(b6 /. b4)] in b6 & [(b6 /. b4),b5] in b7 )
proof end;

theorem Th67: :: PARTFUN2:67
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being Element of b2
for b5 being PartFunc of b1,b2 st b5 = {[b3,b4]} holds
b5 /. b3 = b4
proof end;

theorem Th68: :: PARTFUN2:68
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being PartFunc of b1,b2 st dom b4 = {b3} holds
b4 = {[b3,(b4 /. b3)]}
proof end;

theorem Th69: :: PARTFUN2:69
for b1, b2 being non empty set
for b3 being Element of b1
for b4, b5, b6 being PartFunc of b1,b2 st b4 = b5 /\ b6 & b3 in dom b4 holds
( b4 /. b3 = b5 /. b3 & b4 /. b3 = b6 /. b3 )
proof end;

theorem Th70: :: PARTFUN2:70
for b1, b2 being non empty set
for b3 being Element of b1
for b4, b5, b6 being PartFunc of b1,b2 st b3 in dom b4 & b5 = b4 \/ b6 holds
b5 /. b3 = b4 /. b3
proof end;

theorem Th71: :: PARTFUN2:71
for b1, b2 being non empty set
for b3 being Element of b1
for b4, b5, b6 being PartFunc of b1,b2 st b3 in dom b4 & b5 = b6 \/ b4 holds
b5 /. b3 = b4 /. b3
proof end;

theorem Th72: :: PARTFUN2:72
for b1, b2 being non empty set
for b3 being Element of b1
for b4, b5, b6 being PartFunc of b1,b2 st b3 in dom b4 & b4 = b5 \/ b6 & not b4 /. b3 = b5 /. b3 holds
b4 /. b3 = b6 /. b3
proof end;

theorem Th73: :: PARTFUN2:73
for b1, b2 being non empty set
for b3 being Subset of b1
for b4 being Element of b1
for b5 being PartFunc of b1,b2 holds
( ( b4 in dom b5 & b4 in b3 ) iff [b4,(b5 /. b4)] in b5 | b3 )
proof end;

theorem Th74: :: PARTFUN2:74
for b1, b2 being non empty set
for b3 being Subset of b2
for b4 being Element of b1
for b5 being PartFunc of b1,b2 holds
( ( b4 in dom b5 & b5 /. b4 in b3 ) iff [b4,(b5 /. b4)] in b3 | b5 )
proof end;

theorem Th75: :: PARTFUN2:75
for b1, b2 being non empty set
for b3 being Subset of b2
for b4 being Element of b1
for b5 being PartFunc of b1,b2 holds
( b4 in b5 " b3 iff ( [b4,(b5 /. b4)] in b5 & b5 /. b4 in b3 ) )
proof end;

theorem Th76: :: PARTFUN2:76
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b3,b2 holds
( b4 is_constant_on b1 iff ex b5 being Element of b2 st
for b6 being Element of b3 st b6 in b1 /\ (dom b4) holds
b4 . b6 = b5 )
proof end;

theorem Th77: :: PARTFUN2:77
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b3,b2 holds
( b4 is_constant_on b1 iff for b5, b6 being Element of b3 st b5 in b1 /\ (dom b4) & b6 in b1 /\ (dom b4) holds
b4 . b5 = b4 . b6 )
proof end;

theorem Th78: :: PARTFUN2:78
for b1 being set
for b2, b3 being non empty set
for b4 being Element of b2
for b5 being PartFunc of b3,b2 st b4 in b5 .: b1 holds
ex b6 being Element of b3 st
( b6 in dom b5 & b6 in b1 & b4 = b5 . b6 )
proof end;

theorem Th79: :: PARTFUN2:79
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being Element of b2
for b5 being PartFunc of b1,b2 st b5 is one-to-one holds
( b4 in rng b5 & b3 = (b5 " ) . b4 iff ( b3 in dom b5 & b4 = b5 . b3 ) )
proof end;