begin
:: deftheorem Def1 defines / CFUNCT_1:def 1 :
for C being non empty set
for f1, f2, b4 being PartFunc of C,COMPLEX holds
( b4 = f1 / f2 iff ( dom b4 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b4 holds
b4 /. c = (f1 /. c) * ((f2 /. c) ") ) ) );
:: deftheorem Def2 defines ^ CFUNCT_1:def 2 :
for C being non empty set
for f, b3 being PartFunc of C,COMPLEX holds
( b3 = f ^ iff ( dom b3 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b3 holds
b3 /. c = (f /. c) " ) ) );
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 C,COMPLEX 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
theorem Th60:
theorem
theorem
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem
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 C,COMPLEX 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