:: COMPLSP1 semantic presentation

theorem Th1: :: COMPLSP1:1
canceled;

theorem Th2: :: COMPLSP1:2
canceled;

theorem Th3: :: COMPLSP1:3
0c is_a_unity_wrt addcomplex by BINOP_2:1, SETWISEO:22;

Lemma2: the_unity_wrt addcomplex = 0c
by BINOP_2:1;

theorem Th4: :: COMPLSP1:4
canceled;

theorem Th5: :: COMPLSP1:5
canceled;

theorem Th6: :: COMPLSP1:6
compcomplex is_an_inverseOp_wrt addcomplex
proof end;

theorem Th7: :: COMPLSP1:7
addcomplex has_an_inverseOp by Th6, FINSEQOP:def 2;

theorem Th8: :: COMPLSP1:8
the_inverseOp_wrt addcomplex = compcomplex by Th6, Th7, FINSEQOP:def 3;

definition
canceled;
canceled;
redefine func diffcomplex -> M6([:COMPLEX ,COMPLEX :], COMPLEX ) equals :Def3: :: COMPLSP1:def 3
addcomplex * (id COMPLEX ),compcomplex ;
compatibility
for b1 being M6([:COMPLEX ,COMPLEX :], COMPLEX ) holds
( b1 = diffcomplex iff b1 = addcomplex * (id COMPLEX ),compcomplex )
proof end;
end;

:: deftheorem Def1 COMPLSP1:def 1 :
canceled;

:: deftheorem Def2 COMPLSP1:def 2 :
canceled;

:: deftheorem Def3 defines diffcomplex COMPLSP1:def 3 :
diffcomplex = addcomplex * (id COMPLEX ),compcomplex ;

Lemma7: for b1, b2 being Element of COMPLEX holds diffcomplex . b1,b2 = b1 - b2
by BINOP_2:def 4;

theorem Th9: :: COMPLSP1:9
canceled;

theorem Th10: :: COMPLSP1:10
canceled;

theorem Th11: :: COMPLSP1:11
canceled;

theorem Th12: :: COMPLSP1:12
1r is_a_unity_wrt multcomplex by BINOP_2:6, COMPLEX1:def 7, SETWISEO:22;

theorem Th13: :: COMPLSP1:13
the_unity_wrt multcomplex = 1r by BINOP_2:6, COMPLEX1:def 7;

theorem Th14: :: COMPLSP1:14
canceled;

theorem Th15: :: COMPLSP1:15
multcomplex is_distributive_wrt addcomplex
proof end;

definition
let c1 be complex number ;
canceled;
func c1 multcomplex -> UnOp of COMPLEX equals :: COMPLSP1:def 5
multcomplex [;] a1,(id COMPLEX );
coherence
multcomplex [;] c1,(id COMPLEX ) is UnOp of COMPLEX
proof end;
end;

:: deftheorem Def4 COMPLSP1:def 4 :
canceled;

:: deftheorem Def5 defines multcomplex COMPLSP1:def 5 :
for b1 being complex number holds b1 multcomplex = multcomplex [;] b1,(id COMPLEX );

Lemma10: for b1, b2 being Element of COMPLEX holds (multcomplex [;] b1,(id COMPLEX )) . b2 = b1 * b2
proof end;

theorem Th16: :: COMPLSP1:16
for b1, b2 being Element of COMPLEX holds (b1 multcomplex ) . b2 = b1 * b2 by Lemma10;

theorem Th17: :: COMPLSP1:17
for b1 being Element of COMPLEX holds b1 multcomplex is_distributive_wrt addcomplex by Th15, FINSEQOP:55;

definition
func abscomplex -> Function of COMPLEX , REAL means :Def6: :: COMPLSP1:def 6
for b1 being Element of COMPLEX holds a1 . b1 = |.b1.|;
existence
ex b1 being Function of COMPLEX , REAL st
for b2 being Element of COMPLEX holds b1 . b2 = |.b2.| from FUNCT_2:sch 4();
uniqueness
for b1, b2 being Function of COMPLEX , REAL st ( for b3 being Element of COMPLEX holds b1 . b3 = |.b3.| ) & ( for b3 being Element of COMPLEX holds b2 . b3 = |.b3.| ) holds
b1 = b2 from BINOP_2:sch 1();
end;

:: deftheorem Def6 defines abscomplex COMPLSP1:def 6 :
for b1 being Function of COMPLEX , REAL holds
( b1 = abscomplex iff for b2 being Element of COMPLEX holds b1 . b2 = |.b2.| );

definition
let c1, c2 be FinSequence of COMPLEX ;
func c1 + c2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 7
addcomplex .: a1,a2;
correctness
coherence
addcomplex .: c1,c2 is FinSequence of COMPLEX ;
;
func c1 - c2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 8
diffcomplex .: a1,a2;
correctness
coherence
diffcomplex .: c1,c2 is FinSequence of COMPLEX ;
;
end;

:: deftheorem Def7 defines + COMPLSP1:def 7 :
for b1, b2 being FinSequence of COMPLEX holds b1 + b2 = addcomplex .: b1,b2;

:: deftheorem Def8 defines - COMPLSP1:def 8 :
for b1, b2 being FinSequence of COMPLEX holds b1 - b2 = diffcomplex .: b1,b2;

definition
let c1 be FinSequence of COMPLEX ;
func - c1 -> FinSequence of COMPLEX equals :: COMPLSP1:def 9
compcomplex * a1;
correctness
coherence
compcomplex * c1 is FinSequence of COMPLEX ;
;
end;

:: deftheorem Def9 defines - COMPLSP1:def 9 :
for b1 being FinSequence of COMPLEX holds - b1 = compcomplex * b1;

definition
let c1 be complex number ;
let c2 be FinSequence of COMPLEX ;
func c1 * c2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 10
(a1 multcomplex ) * a2;
correctness
coherence
(c1 multcomplex ) * c2 is FinSequence of COMPLEX ;
;
end;

:: deftheorem Def10 defines * COMPLSP1:def 10 :
for b1 being complex number
for b2 being FinSequence of COMPLEX holds b1 * b2 = (b1 multcomplex ) * b2;

definition
let c1 be FinSequence of COMPLEX ;
func abs c1 -> FinSequence of REAL equals :: COMPLSP1:def 11
abscomplex * a1;
correctness
coherence
abscomplex * c1 is FinSequence of REAL ;
;
end;

:: deftheorem Def11 defines abs COMPLSP1:def 11 :
for b1 being FinSequence of COMPLEX holds abs b1 = abscomplex * b1;

definition
let c1 be Nat;
func COMPLEX c1 -> FinSequence-DOMAIN of COMPLEX equals :: COMPLSP1:def 12
a1 -tuples_on COMPLEX ;
correctness
coherence
c1 -tuples_on COMPLEX is FinSequence-DOMAIN of COMPLEX ;
;
end;

:: deftheorem Def12 defines COMPLEX COMPLSP1:def 12 :
for b1 being Nat holds COMPLEX b1 = b1 -tuples_on COMPLEX ;

registration
let c1 be Nat;
cluster COMPLEX a1 -> ;
coherence
not COMPLEX c1 is empty ;
end;

theorem Th18: :: COMPLSP1:18
for b1 being Nat
for b2 being Element of COMPLEX b1 holds len b2 = b1 by FINSEQ_2:109;

Lemma15: for b1 being Nat
for b2 being Element of COMPLEX b1 holds dom b2 = Seg b1
proof end;

theorem Th19: :: COMPLSP1:19
for b1 being Element of COMPLEX 0 holds b1 = <*> COMPLEX by FINSEQ_2:113;

theorem Th20: :: COMPLSP1:20
<*> COMPLEX is Element of COMPLEX 0 by FINSEQ_2:114;

theorem Th21: :: COMPLSP1:21
for b1, b2 being Nat
for b3 being Element of COMPLEX b2 st b1 in Seg b2 holds
b3 . b1 in COMPLEX
proof end;

theorem Th22: :: COMPLSP1:22
canceled;

theorem Th23: :: COMPLSP1:23
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 st ( for b4 being Nat st b4 in Seg b1 holds
b2 . b4 = b3 . b4 ) holds
b2 = b3 by FINSEQ_2:139;

definition
let c1 be Nat;
let c2, c3 be Element of COMPLEX c1;
redefine func + as c2 + c3 -> Element of COMPLEX a1;
coherence
c2 + c3 is Element of COMPLEX c1 by FINSEQ_2:140;
end;

theorem Th24: :: COMPLSP1:24
for b1, b2 being Nat
for b3, b4 being Element of COMPLEX
for b5, b6 being Element of COMPLEX b2 st b1 in Seg b2 & b3 = b5 . b1 & b4 = b6 . b1 holds
(b5 + b6) . b1 = b3 + b4
proof end;

theorem Th25: :: COMPLSP1:25
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds b2 + b3 = b3 + b2 by FINSEQOP:34;

theorem Th26: :: COMPLSP1:26
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 holds b2 + (b3 + b4) = (b2 + b3) + b4 by FINSEQOP:29;

definition
let c1 be Nat;
func 0c c1 -> FinSequence of COMPLEX equals :: COMPLSP1:def 13
a1 |-> 0c ;
correctness
coherence
c1 |-> 0c is FinSequence of COMPLEX ;
;
end;

:: deftheorem Def13 defines 0c COMPLSP1:def 13 :
for b1 being Nat holds 0c b1 = b1 |-> 0c ;

definition
let c1 be Nat;
redefine func 0c as 0c c1 -> Element of COMPLEX a1;
coherence
0c c1 is Element of COMPLEX c1 ;
end;

theorem Th27: :: COMPLSP1:27
for b1, b2 being Nat st b1 in Seg b2 holds
(0c b2) . b1 = 0c by FINSEQ_2:70;

Lemma21: for b1 being Nat
for b2 being Element of COMPLEX b1 holds b2 + (0c b1) = b2
by Lemma2, FINSEQOP:57;

theorem Th28: :: COMPLSP1:28
for b1 being Nat
for b2 being Element of COMPLEX b1 holds
( b2 + (0c b1) = b2 & b2 = (0c b1) + b2 )
proof end;

definition
let c1 be Nat;
let c2 be Element of COMPLEX c1;
redefine func - as - c2 -> Element of COMPLEX a1;
coherence
- c2 is Element of COMPLEX c1 by FINSEQ_2:133;
end;

theorem Th29: :: COMPLSP1:29
for b1, b2 being Nat
for b3 being Element of COMPLEX
for b4 being Element of COMPLEX b2 st b1 in Seg b2 & b3 = b4 . b1 holds
(- b4) . b1 = - b3
proof end;

Lemma24: for b1 being Nat
for b2 being Element of COMPLEX b1 holds b2 + (- b2) = 0c b1
by Lemma2, Th7, Th8, FINSEQOP:77;

Lemma25: for b1 being Nat holds - (0c b1) = 0c b1
proof end;

theorem Th30: :: COMPLSP1:30
for b1 being Nat
for b2 being Element of COMPLEX b1 holds
( b2 + (- b2) = 0c b1 & (- b2) + b2 = 0c b1 )
proof end;

theorem Th31: :: COMPLSP1:31
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 st b2 + b3 = 0c b1 holds
( b2 = - b3 & b3 = - b2 ) by Lemma2, Th7, Th8, FINSEQOP:78;

theorem Th32: :: COMPLSP1:32
for b1 being Nat
for b2 being Element of COMPLEX b1 holds - (- b2) = b2
proof end;

theorem Th33: :: COMPLSP1:33
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 st - b2 = - b3 holds
b2 = b3
proof end;

Lemma29: for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 st b2 + b3 = b4 + b3 holds
b2 = b4
proof end;

theorem Th34: :: COMPLSP1:34
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 st ( b2 + b3 = b4 + b3 or b2 + b3 = b3 + b4 ) holds
b2 = b4
proof end;

theorem Th35: :: COMPLSP1:35
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds - (b2 + b3) = (- b2) + (- b3)
proof end;

definition
let c1 be Nat;
let c2, c3 be Element of COMPLEX c1;
redefine func - as c2 - c3 -> Element of COMPLEX a1;
coherence
c2 - c3 is Element of COMPLEX c1 by FINSEQ_2:140;
end;

theorem Th36: :: COMPLSP1:36
for b1, b2 being Nat
for b3, b4 being Element of COMPLEX
for b5, b6 being Element of COMPLEX b2 st b1 in Seg b2 & b3 = b5 . b1 & b4 = b6 . b1 holds
(b5 - b6) . b1 = b3 - b4
proof end;

theorem Th37: :: COMPLSP1:37
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds b2 - b3 = b2 + (- b3) by Def3, FINSEQOP:89;

theorem Th38: :: COMPLSP1:38
for b1 being Nat
for b2 being Element of COMPLEX b1 holds b2 - (0c b1) = b2
proof end;

theorem Th39: :: COMPLSP1:39
for b1 being Nat
for b2 being Element of COMPLEX b1 holds (0c b1) - b2 = - b2
proof end;

theorem Th40: :: COMPLSP1:40
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds b2 - (- b3) = b2 + b3
proof end;

theorem Th41: :: COMPLSP1:41
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds - (b2 - b3) = b3 - b2
proof end;

theorem Th42: :: COMPLSP1:42
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds - (b2 - b3) = (- b2) + b3
proof end;

theorem Th43: :: COMPLSP1:43
for b1 being Nat
for b2 being Element of COMPLEX b1 holds b2 - b2 = 0c b1
proof end;

theorem Th44: :: COMPLSP1:44
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 st b2 - b3 = 0c b1 holds
b2 = b3
proof end;

theorem Th45: :: COMPLSP1:45
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 holds (b2 - b3) - b4 = b2 - (b3 + b4)
proof end;

theorem Th46: :: COMPLSP1:46
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 holds b2 + (b3 - b4) = (b2 + b3) - b4
proof end;

theorem Th47: :: COMPLSP1:47
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 holds b2 - (b3 - b4) = (b2 - b3) + b4
proof end;

theorem Th48: :: COMPLSP1:48
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 holds (b2 - b3) + b4 = (b2 + b4) - b3
proof end;

theorem Th49: :: COMPLSP1:49
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds b2 = (b2 + b3) - b3
proof end;

theorem Th50: :: COMPLSP1:50
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds b2 + (b3 - b2) = b3
proof end;

theorem Th51: :: COMPLSP1:51
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds b2 = (b2 - b3) + b3
proof end;

definition
let c1 be Nat;
let c2 be Element of COMPLEX ;
let c3 be Element of COMPLEX c1;
redefine func * as c2 * c3 -> Element of COMPLEX a1;
coherence
c2 * c3 is Element of COMPLEX c1 by FINSEQ_2:133;
end;

theorem Th52: :: COMPLSP1:52
for b1, b2 being Nat
for b3, b4 being Element of COMPLEX
for b5 being Element of COMPLEX b2 st b1 in Seg b2 & b3 = b5 . b1 holds
(b4 * b5) . b1 = b4 * b3
proof end;

theorem Th53: :: COMPLSP1:53
for b1 being Nat
for b2, b3 being Element of COMPLEX
for b4 being Element of COMPLEX b1 holds b2 * (b3 * b4) = (b2 * b3) * b4
proof end;

theorem Th54: :: COMPLSP1:54
for b1 being Nat
for b2, b3 being Element of COMPLEX
for b4 being Element of COMPLEX b1 holds (b2 + b3) * b4 = (b2 * b4) + (b3 * b4)
proof end;

theorem Th55: :: COMPLSP1:55
for b1 being Nat
for b2 being Element of COMPLEX
for b3, b4 being Element of COMPLEX b1 holds b2 * (b3 + b4) = (b2 * b3) + (b2 * b4)
proof end;

theorem Th56: :: COMPLSP1:56
for b1 being Nat
for b2 being Element of COMPLEX b1 holds 1r * b2 = b2
proof end;

theorem Th57: :: COMPLSP1:57
for b1 being Nat
for b2 being Element of COMPLEX b1 holds 0c * b2 = 0c b1
proof end;

theorem Th58: :: COMPLSP1:58
for b1 being Nat
for b2 being Element of COMPLEX b1 holds (- 1r ) * b2 = - b2
proof end;

definition
let c1 be Nat;
let c2 be Element of COMPLEX c1;
redefine func abs as abs c2 -> Element of a1 -tuples_on REAL ;
correctness
coherence
abs c2 is Element of c1 -tuples_on REAL ;
by FINSEQ_2:133;
end;

theorem Th59: :: COMPLSP1:59
for b1, b2 being Nat
for b3 being Element of COMPLEX
for b4 being Element of COMPLEX b2 st b1 in Seg b2 & b3 = b4 . b1 holds
(abs b4) . b1 = |.b3.|
proof end;

theorem Th60: :: COMPLSP1:60
for b1 being Nat holds abs (0c b1) = b1 |-> 0
proof end;

theorem Th61: :: COMPLSP1:61
for b1 being Nat
for b2 being Element of COMPLEX b1 holds abs (- b2) = abs b2
proof end;

theorem Th62: :: COMPLSP1:62
for b1 being Nat
for b2 being Element of COMPLEX
for b3 being Element of COMPLEX b1 holds abs (b2 * b3) = |.b2.| * (abs b3)
proof end;

definition
let c1 be FinSequence of COMPLEX ;
func |.c1.| -> Real equals :: COMPLSP1:def 14
 sqrt (Sum (sqr (abs a1)));
correctness
coherence
sqrt (Sum (sqr (abs c1))) is Real;
;
end;

:: deftheorem Def14 defines |. COMPLSP1:def 14 :
for b1 being FinSequence of COMPLEX holds |.b1.| = sqrt (Sum (sqr (abs b1)));

theorem Th63: :: COMPLSP1:63
for b1 being Nat holds |.(0c b1).| = 0
proof end;

theorem Th64: :: COMPLSP1:64
for b1 being Nat
for b2 being Element of COMPLEX b1 st |.b2.| = 0 holds
b2 = 0c b1
proof end;

theorem Th65: :: COMPLSP1:65
for b1 being Nat
for b2 being Element of COMPLEX b1 holds 0 <= |.b2.|
proof end;

theorem Th66: :: COMPLSP1:66
for b1 being Nat
for b2 being Element of COMPLEX b1 holds |.(- b2).| = |.b2.| by Th61;

theorem Th67: :: COMPLSP1:67
for b1 being Nat
for b2 being Element of COMPLEX
for b3 being Element of COMPLEX b1 holds |.(b2 * b3).| = |.b2.| * |.b3.|
proof end;

Lemma52: for b1, b2 being Nat
for b3 being Element of b1 -tuples_on REAL st b2 in Seg b1 holds
b3 . b2 is Real
proof end;

theorem Th68: :: COMPLSP1:68
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds |.(b2 + b3).| <= |.b2.| + |.b3.|
proof end;

theorem Th69: :: COMPLSP1:69
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds |.(b2 - b3).| <= |.b2.| + |.b3.|
proof end;

theorem Th70: :: COMPLSP1:70
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds |.b2.| - |.b3.| <= |.(b2 + b3).|
proof end;

theorem Th71: :: COMPLSP1:71
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds |.b2.| - |.b3.| <= |.(b2 - b3).|
proof end;

theorem Th72: :: COMPLSP1:72
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds
( |.(b2 - b3).| = 0 iff b2 = b3 )
proof end;

theorem Th73: :: COMPLSP1:73
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 st b2 <> b3 holds
0 < |.(b2 - b3).|
proof end;

theorem Th74: :: COMPLSP1:74
for b1 being Nat
for b2, b3 being Element of COMPLEX b1 holds |.(b2 - b3).| = |.(b3 - b2).|
proof end;

theorem Th75: :: COMPLSP1:75
for b1 being Nat
for b2, b3, b4 being Element of COMPLEX b1 holds |.(b2 - b3).| <= |.(b2 - b4).| + |.(b4 - b3).|
proof end;

definition
let c1 be Nat;
let c2 be Subset of (COMPLEX c1);
attr a2 is open means :Def15: :: COMPLSP1:def 15
for b1 being Element of COMPLEX a1 st b1 in a2 holds
ex b2 being Real st
( 0 < b2 & ( for b3 being Element of COMPLEX a1 st |.b3.| < b2 holds
b1 + b3 in a2 ) );
end;

:: deftheorem Def15 defines open COMPLSP1:def 15 :
for b1 being Nat
for b2 being Subset of (COMPLEX b1) holds
( b2 is open iff for b3 being Element of COMPLEX b1 st b3 in b2 holds
ex b4 being Real st
( 0 < b4 & ( for b5 being Element of COMPLEX b1 st |.b5.| < b4 holds
b3 + b5 in b2 ) ) );

definition
let c1 be Nat;
let c2 be Subset of (COMPLEX c1);
attr a2 is closed means :: COMPLSP1:def 16
for b1 being Element of COMPLEX a1 st ( for b2 being Real st b2 > 0 holds
ex b3 being Element of COMPLEX a1 st
( |.b3.| < b2 & b1 + b3 in a2 ) ) holds
b1 in a2;
end;

:: deftheorem Def16 defines closed COMPLSP1:def 16 :
for b1 being Nat
for b2 being Subset of (COMPLEX b1) holds
( b2 is closed iff for b3 being Element of COMPLEX b1 st ( for b4 being Real st b4 > 0 holds
ex b5 being Element of COMPLEX b1 st
( |.b5.| < b4 & b3 + b5 in b2 ) ) holds
b3 in b2 );

theorem Th76: :: COMPLSP1:76
for b1 being Nat
for b2 being Subset of (COMPLEX b1) st b2 = {} holds
b2 is open
proof end;

theorem Th77: :: COMPLSP1:77
for b1 being Nat
for b2 being Subset of (COMPLEX b1) st b2 = COMPLEX b1 holds
b2 is open
proof end;

theorem Th78: :: COMPLSP1:78
for b1 being Nat
for b2 being Subset-Family of (COMPLEX b1) st ( for b3 being Subset of (COMPLEX b1) st b3 in b2 holds
b3 is open ) holds
for b3 being Subset of (COMPLEX b1) st b3 = union b2 holds
b3 is open
proof end;

theorem Th79: :: COMPLSP1:79
for b1 being Nat
for b2, b3 being Subset of (COMPLEX b1) st b2 is open & b3 is open holds
for b4 being Subset of (COMPLEX b1) st b4 = b2 /\ b3 holds
b4 is open
proof end;

definition
let c1 be Nat;
let c2 be Element of COMPLEX c1;
let c3 be Real;
func Ball c2,c3 -> Subset of (COMPLEX a1) equals :: COMPLSP1:def 17
{ b1 where B is Element of COMPLEX a1 : |.(b1 - a2).| < a3 } ;
coherence
{ b1 where B is Element of COMPLEX c1 : |.(b1 - c2).| < c3 } is Subset of (COMPLEX c1)
proof end;
end;

:: deftheorem Def17 defines Ball COMPLSP1:def 17 :
for b1 being Nat
for b2 being Element of COMPLEX b1
for b3 being Real holds Ball b2,b3 = { b4 where B is Element of COMPLEX b1 : |.(b4 - b2).| < b3 } ;

theorem Th80: :: COMPLSP1:80
for b1 being Nat
for b2 being Real
for b3, b4 being Element of COMPLEX b1 holds
( b3 in Ball b4,b2 iff |.(b4 - b3).| < b2 )
proof end;

theorem Th81: :: COMPLSP1:81
for b1 being Nat
for b2 being Real
for b3 being Element of COMPLEX b1 st 0 < b2 holds
b3 in Ball b3,b2
proof end;

theorem Th82: :: COMPLSP1:82
for b1 being Nat
for b2 being Real
for b3 being Element of COMPLEX b1 holds Ball b3,b2 is open
proof end;

scheme :: COMPLSP1:sch 1
s1{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } :
{ F3(b1) where B is Element of F1() : P1[b1] } is Subset of F2()
proof end;

scheme :: COMPLSP1:sch 2
s2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F3(), P1[ set , set ] } :
{ F4(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] } is Subset of F3()
proof end;

definition
let c1 be Nat;
let c2 be Element of COMPLEX c1;
let c3 be Subset of (COMPLEX c1);
func dist c2,c3 -> Real means :Def18: :: COMPLSP1:def 18
for b1 being Subset of REAL st b1 = { |.(a2 - b2).| where B is Element of COMPLEX a1 : b2 in a3 } holds
a4 = lower_bound b1;
existence
ex b1 being Real st
for b2 being Subset of REAL st b2 = { |.(c2 - b3).| where B is Element of COMPLEX c1 : b3 in c3 } holds
b1 = lower_bound b2
proof end;
uniqueness
for b1, b2 being Real st ( for b3 being Subset of REAL st b3 = { |.(c2 - b4).| where B is Element of COMPLEX c1 : b4 in c3 } holds
b1 = lower_bound b3 ) & ( for b3 being Subset of REAL st b3 = { |.(c2 - b4).| where B is Element of COMPLEX c1 : b4 in c3 } holds
b2 = lower_bound b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines dist COMPLSP1:def 18 :
for b1 being Nat
for b2 being Element of COMPLEX b1
for b3 being Subset of (COMPLEX b1)
for b4 being Real holds
( b4 = dist b2,b3 iff for b5 being Subset of REAL st b5 = { |.(b2 - b6).| where B is Element of COMPLEX b1 : b6 in b3 } holds
b4 = lower_bound b5 );

definition
let c1 be Nat;
let c2 be Subset of (COMPLEX c1);
let c3 be Real;
func Ball c2,c3 -> Subset of (COMPLEX a1) equals :: COMPLSP1:def 19
{ b1 where B is Element of COMPLEX a1 : dist b1,a2 < a3 } ;
coherence
{ b1 where B is Element of COMPLEX c1 : dist b1,c2 < c3 } is Subset of (COMPLEX c1)
proof end;
end;

:: deftheorem Def19 defines Ball COMPLSP1:def 19 :
for b1 being Nat
for b2 being Subset of (COMPLEX b1)
for b3 being Real holds Ball b2,b3 = { b4 where B is Element of COMPLEX b1 : dist b4,b2 < b3 } ;

Lemma67: for b1, b2 being Real st ( for b3 being real number st b3 > 0 holds
b1 + b3 >= b2 ) holds
b1 >= b2
by XREAL_1:43;

theorem Th83: :: COMPLSP1:83
canceled;

theorem Th84: :: COMPLSP1:84
for b1 being Subset of REAL
for b2 being Real st b1 <> {} & ( for b3 being Real st b3 in b1 holds
b2 <= b3 ) holds
lower_bound b1 >= b2
proof end;

theorem Th85: :: COMPLSP1:85
for b1 being Nat
for b2 being Element of COMPLEX b1
for b3 being Subset of (COMPLEX b1) st b3 <> {} holds
dist b2,b3 >= 0
proof end;

theorem Th86: :: COMPLSP1:86
for b1 being Nat
for b2, b3 being Element of COMPLEX b1
for b4 being Subset of (COMPLEX b1) st b4 <> {} holds
dist (b2 + b3),b4 <= (dist b2,b4) + |.b3.|
proof end;

theorem Th87: :: COMPLSP1:87
for b1 being Nat
for b2 being Element of COMPLEX b1
for b3 being Subset of (COMPLEX b1) st b2 in b3 holds
dist b2,b3 = 0
proof end;

theorem Th88: :: COMPLSP1:88
for b1 being Nat
for b2 being Element of COMPLEX b1
for b3 being Subset of (COMPLEX b1) st not b2 in b3 & b3 <> {} & b3 is closed holds
dist b2,b3 > 0
proof end;

theorem Th89: :: COMPLSP1:89
for b1 being Nat
for b2, b3 being Element of COMPLEX b1
for b4 being Subset of (COMPLEX b1) st b4 <> {} holds
|.(b2 - b3).| + (dist b3,b4) >= dist b2,b4
proof end;

theorem Th90: :: COMPLSP1:90
for b1 being Nat
for b2 being Real
for b3 being Element of COMPLEX b1
for b4 being Subset of (COMPLEX b1) holds
( b3 in Ball b4,b2 iff dist b3,b4 < b2 )
proof end;

theorem Th91: :: COMPLSP1:91
for b1 being Nat
for b2 being Real
for b3 being Element of COMPLEX b1
for b4 being Subset of (COMPLEX b1) st 0 < b2 & b3 in b4 holds
b3 in Ball b4,b2
proof end;

theorem Th92: :: COMPLSP1:92
for b1 being Nat
for b2 being Real
for b3 being Subset of (COMPLEX b1) st 0 < b2 holds
b3 c= Ball b3,b2
proof end;

theorem Th93: :: COMPLSP1:93
for b1 being Nat
for b2 being Real
for b3 being Subset of (COMPLEX b1) st b3 <> {} holds
Ball b3,b2 is open
proof end;

definition
let c1 be Nat;
let c2, c3 be Subset of (COMPLEX c1);
func dist c2,c3 -> Real means :Def20: :: COMPLSP1:def 20
for b1 being Subset of REAL st b1 = { |.(b2 - b3).| where B is Element of COMPLEX a1, B is Element of COMPLEX a1 : ( b2 in a2 & b3 in a3 ) } holds
a4 = lower_bound b1;
existence
ex b1 being Real st
for b2 being Subset of REAL st b2 = { |.(b3 - b4).| where B is Element of COMPLEX c1, B is Element of COMPLEX c1 : ( b3 in c2 & b4 in c3 ) } holds
b1 = lower_bound b2
proof end;
uniqueness
for b1, b2 being Real st ( for b3 being Subset of REAL st b3 = { |.(b4 - b5).| where B is Element of COMPLEX c1, B is Element of COMPLEX c1 : ( b4 in c2 & b5 in c3 ) } holds
b1 = lower_bound b3 ) & ( for b3 being Subset of REAL st b3 = { |.(b4 - b5).| where B is Element of COMPLEX c1, B is Element of COMPLEX c1 : ( b4 in c2 & b5 in c3 ) } holds
b2 = lower_bound b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines dist COMPLSP1:def 20 :
for b1 being Nat
for b2, b3 being Subset of (COMPLEX b1)
for b4 being Real holds
( b4 = dist b2,b3 iff for b5 being Subset of REAL st b5 = { |.(b6 - b7).| where B is Element of COMPLEX b1, B is Element of COMPLEX b1 : ( b6 in b2 & b7 in b3 ) } holds
b4 = lower_bound b5 );

definition
let c1, c2 be Subset of REAL ;
func c1 + c2 -> Subset of REAL equals :: COMPLSP1:def 21
{ (b1 + b2) where B is Real, B is Real : ( b1 in a1 & b2 in a2 ) } ;
coherence
{ (b1 + b2) where B is Real, B is Real : ( b1 in c1 & b2 in c2 ) } is Subset of REAL
proof end;
end;

:: deftheorem Def21 defines + COMPLSP1:def 21 :
for b1, b2 being Subset of REAL holds b1 + b2 = { (b3 + b4) where B is Real, B is Real : ( b3 in b1 & b4 in b2 ) } ;

theorem Th94: :: COMPLSP1:94
for b1, b2 being Subset of REAL st b1 <> {} & b2 <> {} holds
b1 + b2 <> {}
proof end;

theorem Th95: :: COMPLSP1:95
for b1, b2 being Subset of REAL st b1 is bounded_below & b2 is bounded_below holds
b1 + b2 is bounded_below
proof end;

theorem Th96: :: COMPLSP1:96
for b1, b2 being Subset of REAL st b1 <> {} & b1 is bounded_below & b2 <> {} & b2 is bounded_below holds
lower_bound (b1 + b2) = (lower_bound b1) + (lower_bound b2)
proof end;

theorem Th97: :: COMPLSP1:97
for b1, b2 being Subset of REAL st b2 is bounded_below & b1 <> {} & ( for b3 being Real st b3 in b1 holds
ex b4 being Real st
( b4 in b2 & b4 <= b3 ) ) holds
lower_bound b1 >= lower_bound b2
proof end;

theorem Th98: :: COMPLSP1:98
for b1 being Nat
for b2, b3 being Subset of (COMPLEX b1) st b2 <> {} & b3 <> {} holds
dist b2,b3 >= 0
proof end;

theorem Th99: :: COMPLSP1:99
for b1 being Nat
for b2, b3 being Subset of (COMPLEX b1) holds dist b2,b3 = dist b3,b2
proof end;

theorem Th100: :: COMPLSP1:100
for b1 being Nat
for b2 being Element of COMPLEX b1
for b3, b4 being Subset of (COMPLEX b1) st b3 <> {} & b4 <> {} holds
(dist b2,b3) + (dist b2,b4) >= dist b3,b4
proof end;

theorem Th101: :: COMPLSP1:101
for b1 being Nat
for b2, b3 being Subset of (COMPLEX b1) st b2 meets b3 holds
dist b2,b3 = 0
proof end;

definition
let c1 be Nat;
func ComplexOpenSets c1 -> Subset-Family of (COMPLEX a1) equals :: COMPLSP1:def 22
{ b1 where B is Subset of (COMPLEX a1) : b1 is open } ;
coherence
{ b1 where B is Subset of (COMPLEX c1) : b1 is open } is Subset-Family of (COMPLEX c1)
proof end;
end;

:: deftheorem Def22 defines ComplexOpenSets COMPLSP1:def 22 :
for b1 being Nat holds ComplexOpenSets b1 = { b2 where B is Subset of (COMPLEX b1) : b2 is open } ;

theorem Th102: :: COMPLSP1:102
for b1 being Nat
for b2 being Subset of (COMPLEX b1) holds
( b2 in ComplexOpenSets b1 iff b2 is open )
proof end;

registration
let c1 be non empty set ;
let c2 be Subset-Family of c1;
cluster TopStruct(# a1,a2 #) -> non empty ;
coherence
not TopStruct(# c1,c2 #) is empty
proof end;
end;

definition
let c1 be Nat;
func the_Complex_Space c1 -> strict TopSpace equals :: COMPLSP1:def 23
 TopStruct(# (COMPLEX a1),(ComplexOpenSets a1) #);
coherence
TopStruct(# (COMPLEX c1),(ComplexOpenSets c1) #) is strict TopSpace
proof end;
end;

:: deftheorem Def23 defines the_Complex_Space COMPLSP1:def 23 :
for b1 being Nat holds the_Complex_Space b1 = TopStruct(# (COMPLEX b1),(ComplexOpenSets b1) #);

registration
let c1 be Nat;
cluster the_Complex_Space a1 -> non empty strict ;
coherence
not the_Complex_Space c1 is empty ;
end;

theorem Th103: :: COMPLSP1:103
for b1 being Nat holds the topology of (the_Complex_Space b1) = ComplexOpenSets b1 ;

theorem Th104: :: COMPLSP1:104
for b1 being Nat holds the carrier of (the_Complex_Space b1) = COMPLEX b1 ;

theorem Th105: :: COMPLSP1:105
for b1 being Nat
for b2 being Point of (the_Complex_Space b1) holds b2 is Element of COMPLEX b1 ;

theorem Th106: :: COMPLSP1:106
canceled;

theorem Th107: :: COMPLSP1:107
canceled;

theorem Th108: :: COMPLSP1:108
for b1 being Nat
for b2 being Subset of (the_Complex_Space b1)
for b3 being Subset of (COMPLEX b1) st b3 = b2 holds
( b3 is open iff b2 is open )
proof end;

theorem Th109: :: COMPLSP1:109
for b1 being Nat
for b2 being Subset of (COMPLEX b1) holds
( b2 is closed iff b2 ` is open )
proof end;

theorem Th110: :: COMPLSP1:110
for b1 being Nat
for b2 being Subset of (the_Complex_Space b1)
for b3 being Subset of (COMPLEX b1) st b3 = b2 holds
( b3 is closed iff b2 is closed )
proof end;

theorem Th111: :: COMPLSP1:111
for b1 being Nat holds the_Complex_Space b1 is_T2
proof end;

theorem Th112: :: COMPLSP1:112
for b1 being Nat holds the_Complex_Space b1 is_T3
proof end;