begin
:: deftheorem Def1 defines / CFUNCT_1:def 1 :
:: deftheorem Def2 defines ^ CFUNCT_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem Th7:
theorem
canceled;
theorem Th9:
Lm1:
for x, Y being set
for C being non empty set
for f being PartFunc of , holds
( x in f " Y iff ( x in dom f & f /. x in Y ) )
by PARTFUN2:44;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
theorem
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th38:
theorem Th39:
theorem
theorem
theorem
canceled;
theorem
theorem Th44:
theorem Th45:
theorem Th46:
Lm2:
(- 1r ) " = - 1r
by COMPLEX1:def 7;
theorem
canceled;
theorem
canceled;
theorem
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem
theorem
for
C being non
empty set for
f1,
f,
f2 being
PartFunc of , holds
(
(f1 / f) + (f2 / f) = (f1 + f2) / f &
(f1 / f) - (f2 / f) = (f1 - f2) / f )
theorem Th60:
theorem
theorem
theorem
theorem Th64:
for
X being
set for
C being non
empty set for
f1,
f2 being
PartFunc of , holds
(
(f1 + f2) | X = (f1 | X) + (f2 | X) &
(f1 + f2) | X = (f1 | X) + f2 &
(f1 + f2) | X = f1 + (f2 | X) )
theorem Th65:
theorem Th66:
theorem
for
X being
set for
C being non
empty set for
f1,
f2 being
PartFunc of , holds
(
(f1 - f2) | X = (f1 | X) - (f2 | X) &
(f1 - f2) | X = (f1 | X) - f2 &
(f1 - f2) | X = f1 - (f2 | X) )
theorem
for
X being
set for
C being non
empty set for
f1,
f2 being
PartFunc of , holds
(
(f1 / f2) | X = (f1 | X) / (f2 | X) &
(f1 / f2) | X = (f1 | X) / f2 &
(f1 / f2) | X = f1 / (f2 | X) )
theorem
begin
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
theorem
theorem
theorem
begin
Lm3:
for C being non empty set
for f being PartFunc of , holds
( |.f.| is bounded iff f is bounded )
theorem Th81:
theorem
theorem
theorem Th84:
theorem
theorem Th86:
theorem Th87:
theorem Th88:
theorem
theorem
theorem Th91:
theorem Th92:
theorem Th93:
theorem
theorem Th95:
theorem
theorem