begin
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem COMPLSP1:def 1 :
canceled;
:: deftheorem COMPLSP1:def 2 :
canceled;
:: deftheorem defines diffcomplex COMPLSP1:def 3 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th15:
:: deftheorem COMPLSP1:def 4 :
canceled;
:: deftheorem defines multcomplex COMPLSP1:def 5 :
Lm1:
for c, c' being Element of COMPLEX holds (multcomplex [;] c,(id COMPLEX )) . c' = c * c'
theorem
theorem
:: deftheorem Def6 defines abscomplex COMPLSP1:def 6 :
:: deftheorem defines + COMPLSP1:def 7 :
:: deftheorem defines - COMPLSP1:def 8 :
:: deftheorem defines - COMPLSP1:def 9 :
:: deftheorem defines * COMPLSP1:def 10 :
:: deftheorem defines abs COMPLSP1:def 11 :
:: deftheorem defines COMPLEX COMPLSP1:def 12 :
Lm2:
for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th21:
theorem
canceled;
theorem
canceled;
theorem Th24:
:: deftheorem defines 0c COMPLSP1:def 13 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th29:
Lm3:
for n being Element of NAT holds - (0c n) = 0c n
theorem
theorem
theorem
theorem
Lm4:
for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
theorem
theorem Th35:
theorem
theorem
canceled;
theorem
theorem
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
:: deftheorem defines |. COMPLSP1:def 14 :
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
Lm5:
for i, j being Element of NAT
for t being Element of i -tuples_on REAL st j in Seg i holds
t . j is Real
theorem Th68:
theorem Th69:
theorem
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
:: deftheorem Def15 defines open COMPLSP1:def 15 :
:: deftheorem defines closed COMPLSP1:def 16 :
theorem
theorem Th77:
theorem Th78:
theorem Th79:
:: deftheorem defines Ball COMPLSP1:def 17 :
theorem Th80:
theorem Th81:
theorem Th82:
:: deftheorem Def18 defines dist COMPLSP1:def 18 :
:: deftheorem defines Ball COMPLSP1:def 19 :
theorem
canceled;
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
:: deftheorem Def20 defines dist COMPLSP1:def 20 :
:: deftheorem defines + COMPLSP1:def 21 :
for
X,
Y being
Subset of holds
X + Y = { (r + r1) where r, r1 is Real : ( r in X & r1 in Y ) } ;
theorem Th94:
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
theorem
theorem Th100:
theorem
:: deftheorem defines ComplexOpenSets COMPLSP1:def 22 :
theorem Th102:
:: deftheorem defines the_Complex_Space COMPLSP1:def 23 :
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th108:
theorem Th109:
theorem Th110:
theorem
theorem