:: XCMPLX_1 semantic presentation

begin


theorem :: XCMPLX_1:1
for a, b, c being complex number holds a + (b + c) = (a + b) + c ;

theorem :: XCMPLX_1:2
for a, c, b being complex number st a + c = b + c holds
a = b ;

theorem :: XCMPLX_1:3
for a, b being complex number st a = a + b holds
b = 0 ;

theorem Th4: :: XCMPLX_1:4
for a, b, c being complex number holds a * (b * c) = (a * b) * c ;

theorem :: XCMPLX_1:5
for c, a, b being complex number st c <> 0 & a * c = b * c holds
a = b
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 & a * c = b * c implies a = b )
assume A1: c <> 0 ; ::_thesis: ( not a * c = b * c or a = b )
assume  a * c = b * c ; ::_thesis: a = b
then  a * (c * (c ")) = (b * c) * (c ") by Th4;
then  a * 1 = (b * c) * (c ") by A1, XCMPLX_0:def_7;
then  a = b * (c * (c ")) ;
then  a = b * 1 by A1, XCMPLX_0:def_7;
hence  a = b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:6
for a, b being complex number holds
( not a * b = 0 or a = 0 or b = 0 ) ;

theorem Th7: :: XCMPLX_1:7
for b, a being complex number st b <> 0 & a * b = b holds
a = 1
proof
let b, a be complex number ; ::_thesis: ( b <> 0 & a * b = b implies a = 1 )
assume that
A1: b <> 0 and
A2: a * b = b ; ::_thesis: a = 1
 (a * b) * (b ") = 1 by A1, A2, XCMPLX_0:def_7;
then  a * 1 = 1 by A2, Th4;
hence  a = 1 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:8
for a, b, c being complex number holds a * (b + c) = (a * b) + (a * c) ;

theorem :: XCMPLX_1:9
for a, b, c, d being complex number holds ((a + b) + c) * d = ((a * d) + (b * d)) + (c * d) ;

theorem :: XCMPLX_1:10
for a, b, c, d being complex number holds (a + b) * (c + d) = (((a * c) + (a * d)) + (b * c)) + (b * d) ;

theorem :: XCMPLX_1:11
for a being complex number holds 2 * a = a + a ;

theorem :: XCMPLX_1:12
for a being complex number holds 3 * a = (a + a) + a ;

theorem :: XCMPLX_1:13
for a being complex number holds 4 * a = ((a + a) + a) + a ;

theorem :: XCMPLX_1:14
for a being complex number holds a - a = 0 ;

theorem :: XCMPLX_1:15
for a, b being complex number st a - b = 0 holds
a = b ;

theorem :: XCMPLX_1:16
for b, a being complex number st b - a = b holds
a = 0 ;

theorem :: XCMPLX_1:17
for a, b being complex number holds a = a - (b - b) ;

theorem :: XCMPLX_1:18
for a, b being complex number holds a - (a - b) = b ;

theorem :: XCMPLX_1:19
for a, c, b being complex number st a - c = b - c holds
a = b ;

theorem :: XCMPLX_1:20
for c, a, b being complex number st c - a = c - b holds
a = b ;

theorem :: XCMPLX_1:21
for a, b, c being complex number holds (a - b) - c = (a - c) - b ;

theorem :: XCMPLX_1:22
for a, c, b being complex number holds a - c = (a - b) - (c - b) ;

theorem :: XCMPLX_1:23
for c, a, b being complex number holds (c - a) - (c - b) = b - a ;

theorem :: XCMPLX_1:24
for a, b, c, d being complex number st a - b = c - d holds
a - c = b - d ;

Lm1:  for a, b being complex number holds (a ") * (b ") = (a * b) "
proof
let a, b be complex number ; ::_thesis: (a ") * (b ") = (a * b) "
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
supposeA1: ( a = 0 or b = 0 ) ; ::_thesis: (a ") * (b ") = (a * b) "
then  ( a " = 0 or b " = 0 ) ;
hence  (a ") * (b ") = (a * b) " by A1; ::_thesis: verum
end;
supposethat A2: a <> 0 and
A3: b <> 0 ; ::_thesis: (a ") * (b ") = (a * b) "
thus (a ") * (b ") = ((a ") * (b ")) * 1
.= ((a ") * (b ")) * ((a * b) * ((a * b) ")) by A2, A3, XCMPLX_0:def_7
.= (((a ") * a) * ((b ") * b)) * ((a * b) ")
.= (1 * ((b ") * b)) * ((a * b) ") by A2, XCMPLX_0:def_7
.= 1 * ((a * b) ") by A3, XCMPLX_0:def_7
.= (a * b) " ; ::_thesis: verum
end;
end;
end;

Lm2:  for a, b, c being complex number holds a / (b / c) = (a * c) / b
proof
let a, b, c be complex number ; ::_thesis: a / (b / c) = (a * c) / b
thus a / (b / c) = a / (b * (c ")) by XCMPLX_0:def_9
.= a * ((b * (c ")) ") by XCMPLX_0:def_9
.= a * ((b ") * ((c ") ")) by Lm1
.= (a * c) * (b ")
.= (a * c) / b by XCMPLX_0:def_9 ; ::_thesis: verum
end;

Lm3:  for b, a being complex number st b <> 0 holds
(a / b) * b = a
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies (a / b) * b = a )
assume A1: b <> 0 ; ::_thesis: (a / b) * b = a
thus (a / b) * b = (a * (b ")) * b by XCMPLX_0:def_9
.= a * ((b ") * b)
.= a * 1 by A1, XCMPLX_0:def_7
.= a ; ::_thesis: verum
end;

Lm4:  for a being complex number holds 1 / a = a "
proof
let a be complex number ; ::_thesis: 1 / a = a "
thus 1 / a = 1 * (a ") by XCMPLX_0:def_9
.= a " ; ::_thesis: verum
end;

Lm5:  for a being complex number st a <> 0 holds
a / a = 1
proof
let a be complex number ; ::_thesis: ( a <> 0 implies a / a = 1 )
assume A1: a <> 0 ; ::_thesis: a / a = 1
thus a / a = a * (a ") by XCMPLX_0:def_9
.= 1 by A1, XCMPLX_0:def_7 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:25
for a, b being complex number holds a = a + (b - b) ;

theorem :: XCMPLX_1:26
for a, b being complex number holds a = (a + b) - b ;

theorem :: XCMPLX_1:27
for a, b being complex number holds a = (a - b) + b ;

theorem :: XCMPLX_1:28
for a, c, b being complex number holds a + c = (a + b) + (c - b) ;

theorem :: XCMPLX_1:29
for a, b, c being complex number holds (a + b) - c = (a - c) + b ;

theorem :: XCMPLX_1:30
for a, b, c being complex number holds (a - b) + c = (c - b) + a ;

theorem :: XCMPLX_1:31
for a, c, b being complex number holds a + c = (a + b) - (b - c) ;

theorem :: XCMPLX_1:32
for a, c, b being complex number holds a - c = (a + b) - (c + b) ;

theorem :: XCMPLX_1:33
for a, b, c, d being complex number st a + b = c + d holds
a - c = d - b ;

theorem :: XCMPLX_1:34
for a, c, d, b being complex number st a - c = d - b holds
a + b = c + d ;

theorem :: XCMPLX_1:35
for a, b, c, d being complex number st a + b = c - d holds
a + d = c - b ;

theorem :: XCMPLX_1:36
for a, b, c being complex number holds a - (b + c) = (a - b) - c ;

theorem :: XCMPLX_1:37
for a, b, c being complex number holds a - (b - c) = (a - b) + c ;

theorem :: XCMPLX_1:38
for a, b, c being complex number holds a - (b - c) = a + (c - b) ;

theorem :: XCMPLX_1:39
for a, c, b being complex number holds a - c = (a - b) + (b - c) ;

theorem :: XCMPLX_1:40
for a, b, c being complex number holds a * (b - c) = (a * b) - (a * c) ;

theorem :: XCMPLX_1:41
for a, b, c, d being complex number holds (a - b) * (c - d) = (b - a) * (d - c) ;

theorem :: XCMPLX_1:42
for a, b, c, d being complex number holds ((a - b) - c) * d = ((a * d) - (b * d)) - (c * d) ;

theorem :: XCMPLX_1:43
for a, b, c, d being complex number holds ((a + b) - c) * d = ((a * d) + (b * d)) - (c * d) ;

theorem :: XCMPLX_1:44
for a, b, c, d being complex number holds ((a - b) + c) * d = ((a * d) - (b * d)) + (c * d) ;

theorem :: XCMPLX_1:45
for a, b, c, d being complex number holds (a + b) * (c - d) = (((a * c) - (a * d)) + (b * c)) - (b * d) ;

theorem :: XCMPLX_1:46
for a, b, c, d being complex number holds (a - b) * (c + d) = (((a * c) + (a * d)) - (b * c)) - (b * d) ;

theorem :: XCMPLX_1:47
for a, b, e, d being complex number holds (a - b) * (e - d) = (((a * e) - (a * d)) - (b * e)) + (b * d) ;

theorem :: XCMPLX_1:48
for a, b, c being complex number holds (a / b) / c = (a / c) / b
proof
let a, b, c be complex number ; ::_thesis: (a / b) / c = (a / c) / b
thus (a / b) / c = (a * (b ")) / c by XCMPLX_0:def_9
.= (a * (b ")) * (c ") by XCMPLX_0:def_9
.= (a * (c ")) * (b ")
.= (a / c) * (b ") by XCMPLX_0:def_9
.= (a / c) / b by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem Th49: :: XCMPLX_1:49
for a being complex number holds a / 0 = 0
proof
let a be complex number ; ::_thesis: a / 0 = 0
thus a / 0 = a * (0 ") by XCMPLX_0:def_9
.= 0 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:50
for a, b being complex number st a <> 0 & b <> 0 holds
a / b <> 0 ;

theorem :: XCMPLX_1:51
for b, a being complex number st b <> 0 holds
a = a / (b / b)
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a / (b / b) )
A1: a = a / 1 ;
assume  b <> 0 ; ::_thesis: a = a / (b / b)
hence  a = a / (b / b) by A1, Lm5; ::_thesis: verum
end;

Lm6:  for a, b, c, d being complex number holds (a / b) * (c / d) = (a * c) / (b * d)
proof
let a, b, c, d be complex number ; ::_thesis: (a / b) * (c / d) = (a * c) / (b * d)
thus (a / b) * (c / d) = (a * (b ")) * (c / d) by XCMPLX_0:def_9
.= (a * (b ")) * (c * (d ")) by XCMPLX_0:def_9
.= (a * c) * ((b ") * (d "))
.= (a * c) * ((b * d) ") by Lm1
.= (a * c) / (b * d) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

Lm7:  for a, b being complex number holds (a / b) " = b / a
proof
let a, b be complex number ; ::_thesis: (a / b) " = b / a
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
supposeA1: a = 0 ; ::_thesis: (a / b) " = b / a
hence (a / b) " = b * (0 ")
.= b / a by A1, XCMPLX_0:def_9 ;
::_thesis: verum
end;
supposeA2: b = 0 ; ::_thesis: (a / b) " = b / a
hence (a / b) " = (a * (0 ")) " by XCMPLX_0:def_9
.= b / a by A2 ;
::_thesis: verum
end;
supposeA3: ( a <> 0 & b <> 0 ) ; ::_thesis: (a / b) " = b / a
 (a / b) * (b / a) = (a * b) / (a * b) by Lm6;
then  (a / b) * (b / a) = 1 by A3, Lm5;
hence  (a / b) " = b / a by A3, XCMPLX_0:def_7; ::_thesis: verum
end;
end;
end;

Lm8:  for a, b, c being complex number holds a * (b / c) = (a * b) / c
proof
let a, b, c be complex number ; ::_thesis: a * (b / c) = (a * b) / c
thus a * (b / c) = (a / 1) * (b / c)
.= (a * b) / (1 * c) by Lm6
.= (a * b) / c ; ::_thesis: verum
end;

theorem :: XCMPLX_1:52
for a, b being complex number st a <> 0 holds
a / (a / b) = b
proof
let a, b be complex number ; ::_thesis: ( a <> 0 implies a / (a / b) = b )
assume A1: a <> 0 ; ::_thesis: a / (a / b) = b
thus a / (a / b) = a * ((a / b) ") by XCMPLX_0:def_9
.= a * (b / a) by Lm7
.= (a * b) / a by Lm8
.= (a / a) * b by Lm8
.= 1 * b by A1, Lm5
.= b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:53
for c, a, b being complex number st c <> 0 & a / c = b / c holds
a = b
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 & a / c = b / c implies a = b )
assume that
A1: c <> 0 and
A2: a / c = b / c ; ::_thesis: a = b
 a = (b / c) * c by A1, A2, Lm3;
hence  a = b by A1, Lm3; ::_thesis: verum
end;

Lm9:  for b, a being complex number st b <> 0 holds
a = (a * b) / b
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * b) / b )
A1: a = a * 1 ;
assume  b <> 0 ; ::_thesis: a = (a * b) / b
then  a = a * (b / b) by A1, Lm5;
then  a = a * (b * (b ")) by XCMPLX_0:def_9;
then  a = (a * b) * (b ") ;
hence  a = (a * b) / b by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XCMPLX_1:54
for a, b being complex number st a / b <> 0 holds
b = a / (a / b)
proof
let a, b be complex number ; ::_thesis: ( a / b <> 0 implies b = a / (a / b) )
assume A1: a / b <> 0 ; ::_thesis: b = a / (a / b)
then  b <> 0 by Th49;
then  (a / b) * b = a by Lm3;
hence  b = a / (a / b) by A1, Lm9; ::_thesis: verum
end;

Lm10:  for c, a, b being complex number st c <> 0 holds
a / b = (a * c) / (b * c)
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a * c) / (b * c) )
assume A1: c <> 0 ; ::_thesis: a / b = (a * c) / (b * c)
thus a / b = (a * (b ")) * 1 by XCMPLX_0:def_9
.= (a * (b ")) * (c * (c ")) by A1, XCMPLX_0:def_7
.= (a * c) * ((b ") * (c "))
.= (a * c) * ((b * c) ") by Lm1
.= (a * c) / (b * c) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:55
for c, a, b being complex number st c <> 0 holds
a / b = (a / c) / (b / c)
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a / c) / (b / c) )
assume  c <> 0 ; ::_thesis: a / b = (a / c) / (b / c)
hence a / b = (a * (c ")) / (b * (c ")) by Lm10
.= (a / c) / (b * (c ")) by XCMPLX_0:def_9
.= (a / c) / (b / c) by XCMPLX_0:def_9 ;
::_thesis: verum
end;

theorem :: XCMPLX_1:56
for a being complex number holds 1 / (1 / a) = a
proof
let a be complex number ; ::_thesis: 1 / (1 / a) = a
thus 1 / (1 / a) = (1 * a) / 1 by Lm2
.= a ; ::_thesis: verum
end;

Lm11:  for a, b being complex number holds (a * (b ")) " = (a ") * b
proof
let a, b be complex number ; ::_thesis: (a * (b ")) " = (a ") * b
thus (a * (b ")) " = (a ") * ((b ") ") by Lm1
.= (a ") * b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:57
for a, b being complex number holds 1 / (a / b) = b / a
proof
let a, b be complex number ; ::_thesis: 1 / (a / b) = b / a
thus 1 / (a / b) = 1 / (a * (b ")) by XCMPLX_0:def_9
.= (a * (b ")) " by Lm4
.= b * (a ") by Lm11
.= b / a by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem Th58: :: XCMPLX_1:58
for a, b being complex number st a / b = 1 holds
a = b
proof
let a, b be complex number ; ::_thesis: ( a / b = 1 implies a = b )
assume A1: a / b = 1 ; ::_thesis: a = b
then  b <> 0 by Th49;
then  a = 1 * b by A1, Lm3;
hence  a = b ; ::_thesis: verum
end;

Lm12:  for a, b being complex number st a " = b " holds
a = b
proof
let a, b be complex number ; ::_thesis: ( a " = b " implies a = b )
assume  a " = b " ; ::_thesis: a = b
then  a = (b ") " ;
hence  a = b ; ::_thesis: verum
end;

theorem Th59: :: XCMPLX_1:59
for a, b being complex number st 1 / a = 1 / b holds
a = b
proof
let a, b be complex number ; ::_thesis: ( 1 / a = 1 / b implies a = b )
assume  1 / a = 1 / b ; ::_thesis: a = b
then  a " = 1 / b by Lm4;
then  a " = b " by Lm4;
hence  a = b by Lm12; ::_thesis: verum
end;

theorem :: XCMPLX_1:60
for a being complex number st a <> 0 holds
a / a = 1 by Lm5;

theorem :: XCMPLX_1:61
for b, a being complex number st b <> 0 & b / a = b holds
a = 1
proof
let b, a be complex number ; ::_thesis: ( b <> 0 & b / a = b implies a = 1 )
assume that
A1: b <> 0 and
A2: b / a = b ; ::_thesis: a = 1
 a <> 0 by A1, A2, Th49;
then  b = b * a by A2, Lm3;
hence  a = 1 by A1, Th7; ::_thesis: verum
end;

theorem Th62: :: XCMPLX_1:62
for a, c, b being complex number holds (a / c) + (b / c) = (a + b) / c
proof
let a, c, b be complex number ; ::_thesis: (a / c) + (b / c) = (a + b) / c
thus (a / c) + (b / c) = (a * (c ")) + (b / c) by XCMPLX_0:def_9
.= (a * (c ")) + (b * (c ")) by XCMPLX_0:def_9
.= (a + b) * (c ")
.= (a + b) / c by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:63
for a, b, e, d being complex number holds ((a + b) + e) / d = ((a / d) + (b / d)) + (e / d)
proof
let a, b, e, d be complex number ; ::_thesis: ((a + b) + e) / d = ((a / d) + (b / d)) + (e / d)
thus ((a + b) + e) / d = ((a + b) / d) + (e / d) by Th62
.= ((a / d) + (b / d)) + (e / d) by Th62 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:64
for a being complex number holds (a + a) / 2 = a ;

theorem :: XCMPLX_1:65
for a being complex number holds (a / 2) + (a / 2) = a ;

theorem :: XCMPLX_1:66
for a, b being complex number st a = (a + b) / 2 holds
a = b ;

theorem :: XCMPLX_1:67
for a being complex number holds ((a + a) + a) / 3 = a ;

theorem :: XCMPLX_1:68
for a being complex number holds ((a / 3) + (a / 3)) + (a / 3) = a ;

theorem :: XCMPLX_1:69
for a being complex number holds (((a + a) + a) + a) / 4 = a ;

theorem :: XCMPLX_1:70
for a being complex number holds (((a / 4) + (a / 4)) + (a / 4)) + (a / 4) = a ;

theorem :: XCMPLX_1:71
for a being complex number holds (a / 4) + (a / 4) = a / 2 ;

theorem :: XCMPLX_1:72
for a being complex number holds (a + a) / 4 = a / 2 ;

theorem :: XCMPLX_1:73
for a, b being complex number st a * b = 1 holds
a = 1 / b
proof
let a, b be complex number ; ::_thesis: ( a * b = 1 implies a = 1 / b )
assume A1: a * b = 1 ; ::_thesis: a = 1 / b
then  b <> 0 ;
then  a * 1 = 1 * (b ") by A1, XCMPLX_0:def_7;
hence  a = 1 / b by Lm4; ::_thesis: verum
end;

theorem :: XCMPLX_1:74
for a, b, c being complex number holds a * (b / c) = (a * b) / c by Lm8;

theorem :: XCMPLX_1:75
for a, b, e being complex number holds (a / b) * e = (e / b) * a
proof
let a, b, e be complex number ; ::_thesis: (a / b) * e = (e / b) * a
thus (a / b) * e = (a * e) / b by Lm8
.= (e / b) * a by Lm8 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:76
for a, b, c, d being complex number holds (a / b) * (c / d) = (a * c) / (b * d) by Lm6;

theorem :: XCMPLX_1:77
for a, b, c being complex number holds a / (b / c) = (a * c) / b by Lm2;

Lm13:  for a, b, c, d being complex number holds (a / b) / (c / d) = (a * d) / (b * c)
proof
let a, b, c, d be complex number ; ::_thesis: (a / b) / (c / d) = (a * d) / (b * c)
thus (a / b) / (c / d) = (a / b) * ((c / d) ") by XCMPLX_0:def_9
.= (a / b) * (d / c) by Lm7
.= (a * d) / (b * c) by Lm6 ; ::_thesis: verum
end;

theorem Th78: :: XCMPLX_1:78
for a, b, c being complex number holds a / (b * c) = (a / b) / c
proof
let a, b, c be complex number ; ::_thesis: a / (b * c) = (a / b) / c
thus a / (b * c) = (a * 1) / (b * c)
.= (a / b) / (c / 1) by Lm13
.= (a / b) / c ; ::_thesis: verum
end;

theorem :: XCMPLX_1:79
for a, b, c being complex number holds a / (b / c) = a * (c / b)
proof
let a, b, c be complex number ; ::_thesis: a / (b / c) = a * (c / b)
thus a / (b / c) = (a * c) / b by Lm2
.= (a * c) * (b ") by XCMPLX_0:def_9
.= a * (c * (b "))
.= a * (c / b) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:80
for a, b, c being complex number holds a / (b / c) = (c / b) * a
proof
let a, b, c be complex number ; ::_thesis: a / (b / c) = (c / b) * a
a / (b / c) = (a * c) / b by Lm2
.= (a * c) * (b ") by XCMPLX_0:def_9
.= a * (c * (b "))
.= a * (c / b) by XCMPLX_0:def_9 ;
hence  a / (b / c) = (c / b) * a ; ::_thesis: verum
end;

theorem Th81: :: XCMPLX_1:81
for a, b, e being complex number holds a / (b / e) = e * (a / b)
proof
let a, b, e be complex number ; ::_thesis: a / (b / e) = e * (a / b)
thus a / (b / e) = (a * e) / b by Lm2
.= (e * a) * (b ") by XCMPLX_0:def_9
.= e * (a * (b "))
.= e * (a / b) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:82
for a, b, c being complex number holds a / (b / c) = (a / b) * c
proof
let a, b, c be complex number ; ::_thesis: a / (b / c) = (a / b) * c
a / (b / c) = (a * c) / b by Lm2
.= (c * a) * (b ") by XCMPLX_0:def_9
.= c * (a * (b "))
.= c * (a / b) by XCMPLX_0:def_9 ;
hence  a / (b / c) = (a / b) * c ; ::_thesis: verum
end;

Lm14:  for a, b being complex number holds a * (1 / b) = a / b
proof
let a, b be complex number ; ::_thesis: a * (1 / b) = a / b
thus a / b = a * (b ") by XCMPLX_0:def_9
.= a * (1 / b) by Lm4 ; ::_thesis: verum
end;

Lm15:  for c, a, b being complex number holds (1 / c) * (a / b) = a / (b * c)
proof
let c, a, b be complex number ; ::_thesis: (1 / c) * (a / b) = a / (b * c)
(a / b) / c = (c ") * (a / b) by XCMPLX_0:def_9
.= (1 / c) * (a / b) by Lm4 ;
hence  (1 / c) * (a / b) = a / (b * c) by Th78; ::_thesis: verum
end;

theorem :: XCMPLX_1:83
for a, b, c, d being complex number holds (a * b) / (c * d) = ((a / c) * b) / d
proof
let a, b, c, d be complex number ; ::_thesis: (a * b) / (c * d) = ((a / c) * b) / d
thus (a * b) / (c * d) = (1 / c) * ((a * b) / d) by Lm15
.= ((1 / c) * (a * b)) / d by Lm8
.= (((1 / c) * a) * b) / d
.= ((a / c) * b) / d by Lm14 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:84
for a, b, c, d being complex number holds (a / b) / (c / d) = (a * d) / (b * c) by Lm13;

theorem :: XCMPLX_1:85
for a, c, b, d being complex number holds (a / c) * (b / d) = (a / d) * (b / c)
proof
let a, c, b, d be complex number ; ::_thesis: (a / c) * (b / d) = (a / d) * (b / c)
thus (a / c) * (b / d) = (a * b) / (d * c) by Lm6
.= (a / d) * (b / c) by Lm6 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:86
for a, b, c, d, e being complex number holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
proof
let a, b, c, d, e be complex number ; ::_thesis: a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
thus a / ((b * c) * (d / e)) = a / ((b * c) * (d * (e "))) by XCMPLX_0:def_9
.= a / (c * ((b * d) * (e ")))
.= a / (c * ((b * d) / e)) by XCMPLX_0:def_9
.= a / ((b * d) / (e / c)) by Th81
.= (e / c) * (a / (b * d)) by Th81 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:87
for b, a being complex number st b <> 0 holds
(a / b) * b = a by Lm3;

theorem :: XCMPLX_1:88
for b, a being complex number st b <> 0 holds
a = a * (b / b)
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a * (b / b) )
A1: a = a * 1 ;
assume  b <> 0 ; ::_thesis: a = a * (b / b)
hence  a = a * (b / b) by A1, Lm5; ::_thesis: verum
end;

theorem :: XCMPLX_1:89
for b, a being complex number st b <> 0 holds
a = (a * b) / b by Lm9;

theorem :: XCMPLX_1:90
for b, a, c being complex number st b <> 0 holds
a * c = (a * b) * (c / b)
proof
let b, a, c be complex number ; ::_thesis: ( b <> 0 implies a * c = (a * b) * (c / b) )
assume A1: b <> 0 ; ::_thesis: a * c = (a * b) * (c / b)
thus a * c = (a * 1) * c
.= (a * (b * (b "))) * c by A1, XCMPLX_0:def_7
.= (a * b) * ((b ") * c)
.= (a * b) * (c / b) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:91
for c, a, b being complex number st c <> 0 holds
a / b = (a * c) / (b * c) by Lm10;

theorem :: XCMPLX_1:92
for c, a, b being complex number st c <> 0 holds
a / b = (a / (b * c)) * c
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a / (b * c)) * c )
assume A1: c <> 0 ; ::_thesis: a / b = (a / (b * c)) * c
c * (a / (b * c)) = c * ((a * 1) / (b * c))
.= c * ((1 / c) * (a / b)) by Lm6
.= ((1 / c) * c) * (a / b)
.= 1 * (a / b) by A1, Lm3
.= a / b ;
hence  a / b = (a / (b * c)) * c ; ::_thesis: verum
end;

theorem :: XCMPLX_1:93
for b, a, c being complex number st b <> 0 holds
a * c = (a * b) / (b / c)
proof
let b, a, c be complex number ; ::_thesis: ( b <> 0 implies a * c = (a * b) / (b / c) )
assume A1: b <> 0 ; ::_thesis: a * c = (a * b) / (b / c)
thus a * c = (a * 1) * c
.= (a * (b * (b "))) * c by A1, XCMPLX_0:def_7
.= (a * b) * ((b ") * c)
.= (a * b) * ((b * (c ")) ") by Lm11
.= (a * b) / (b * (c ")) by XCMPLX_0:def_9
.= (a * b) / (b / c) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem Th94: :: XCMPLX_1:94
for c, d, a, b being complex number st c <> 0 & d <> 0 & a * c = b * d holds
a / d = b / c
proof
let c, d, a, b be complex number ; ::_thesis: ( c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c )
assume that
A1: c <> 0 and
A2: d <> 0 ; ::_thesis: ( not a * c = b * d or a / d = b / c )
assume  a * c = b * d ; ::_thesis: a / d = b / c
then  a = (b * d) / c by A1, Lm9;
then  a = d * (b / c) by Lm8;
hence  a / d = b / c by A2, Lm9; ::_thesis: verum
end;

theorem Th95: :: XCMPLX_1:95
for c, d, a, b being complex number st c <> 0 & d <> 0 & a / d = b / c holds
a * c = b * d
proof
let c, d, a, b be complex number ; ::_thesis: ( c <> 0 & d <> 0 & a / d = b / c implies a * c = b * d )
assume that
A1: c <> 0 and
A2: d <> 0 and
A3: a / d = b / c ; ::_thesis: a * c = b * d
 c * (a / d) = b by A1, A3, Lm3;
then  (a * c) / d = b by Lm8;
hence  a * c = b * d by A2, Lm3; ::_thesis: verum
end;

theorem :: XCMPLX_1:96
for c, d, a, b being complex number st c <> 0 & d <> 0 & a * c = b / d holds
a * d = b / c
proof
let c, d, a, b be complex number ; ::_thesis: ( c <> 0 & d <> 0 & a * c = b / d implies a * d = b / c )
assume that
A1: c <> 0 and
A2: d <> 0 ; ::_thesis: ( not a * c = b / d or a * d = b / c )
assume  a * c = b / d ; ::_thesis: a * d = b / c
then  (a * c) * d = b by A2, Lm3;
then  (a * d) * c = b ;
hence  a * d = b / c by A1, Lm9; ::_thesis: verum
end;

theorem :: XCMPLX_1:97
for c, a, b being complex number st c <> 0 holds
a / b = c * ((a / c) / b)
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = c * ((a / c) / b) )
assume A1: c <> 0 ; ::_thesis: a / b = c * ((a / c) / b)
thus a / b = a * (b ") by XCMPLX_0:def_9
.= (c * (a / c)) * (b ") by A1, Lm3
.= c * ((a / c) * (b "))
.= c * ((a / c) / b) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:98
for c, a, b being complex number st c <> 0 holds
a / b = (a / c) * (c / b)
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a / c) * (c / b) )
assume A1: c <> 0 ; ::_thesis: a / b = (a / c) * (c / b)
thus a / b = a * (b ") by XCMPLX_0:def_9
.= ((a / c) * c) * (b ") by A1, Lm3
.= (a / c) * (c * (b "))
.= (a / c) * (c / b) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:99
for a, b being complex number holds a * (1 / b) = a / b by Lm14;

Lm16:  for a being complex number holds 1 / (a ") = a
proof
let a be complex number ; ::_thesis: 1 / (a ") = a
1 / (a ") = (a ") " by Lm4
.= a ;
hence  1 / (a ") = a ; ::_thesis: verum
end;

theorem :: XCMPLX_1:100
for a, b being complex number holds a / (1 / b) = a * b
proof
let a, b be complex number ; ::_thesis: a / (1 / b) = a * b
thus a / (1 / b) = a / (b ") by Lm4
.= a * (1 / (b ")) by Lm14
.= a * b by Lm16 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:101
for a, b, c being complex number holds (a / b) * c = ((1 / b) * c) * a
proof
let a, b, c be complex number ; ::_thesis: (a / b) * c = ((1 / b) * c) * a
 (a / b) * c = ((1 / b) * a) * c by Lm14;
hence  (a / b) * c = ((1 / b) * c) * a ; ::_thesis: verum
end;

theorem :: XCMPLX_1:102
for a, b being complex number holds (1 / a) * (1 / b) = 1 / (a * b)
proof
let a, b be complex number ; ::_thesis: (1 / a) * (1 / b) = 1 / (a * b)
thus (1 / a) * (1 / b) = (a ") * (1 / b) by Lm4
.= (a ") * (b ") by Lm4
.= (a * b) " by Lm1
.= 1 / (a * b) by Lm4 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:103
for c, a, b being complex number holds (1 / c) * (a / b) = a / (b * c) by Lm15;

theorem :: XCMPLX_1:104
for a, b, c being complex number holds (a / b) / c = (1 / b) * (a / c)
proof
let a, b, c be complex number ; ::_thesis: (a / b) / c = (1 / b) * (a / c)
(a / b) / c = (a * (b ")) / c by XCMPLX_0:def_9
.= (a * (b ")) * (c ") by XCMPLX_0:def_9
.= (a * (c ")) * (b ")
.= (a / c) * (b ") by XCMPLX_0:def_9
.= (a / c) / b by XCMPLX_0:def_9 ;
hence (a / b) / c = (b ") * (a / c) by XCMPLX_0:def_9
.= (1 / b) * (a / c) by Lm4 ;
::_thesis: verum
end;

theorem :: XCMPLX_1:105
for a, b, c being complex number holds (a / b) / c = (1 / c) * (a / b)
proof
let a, b, c be complex number ; ::_thesis: (a / b) / c = (1 / c) * (a / b)
thus (a / b) / c = (c ") * (a / b) by XCMPLX_0:def_9
.= (1 / c) * (a / b) by Lm4 ; ::_thesis: verum
end;

theorem Th106: :: XCMPLX_1:106
for a being complex number st a <> 0 holds
a * (1 / a) = 1
proof
let a be complex number ; ::_thesis: ( a <> 0 implies a * (1 / a) = 1 )
assume A1: a <> 0 ; ::_thesis: a * (1 / a) = 1
thus a * (1 / a) = a * (a ") by Lm4
.= 1 by A1, XCMPLX_0:def_7 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:107
for b, a being complex number st b <> 0 holds
a = (a * b) * (1 / b)
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * b) * (1 / b) )
A1: a = a * 1 ;
assume  b <> 0 ; ::_thesis: a = (a * b) * (1 / b)
then  a = a * (b / b) by A1, Lm5;
then a = a * (b * (b ")) by XCMPLX_0:def_9
.= a * (b * (1 / b)) by Lm4 ;
hence  a = (a * b) * (1 / b) ; ::_thesis: verum
end;

theorem :: XCMPLX_1:108
for b, a being complex number st b <> 0 holds
a = a * ((1 / b) * b)
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a * ((1 / b) * b) )
assume A1: b <> 0 ; ::_thesis: a = a * ((1 / b) * b)
thus a = a * 1
.= a * ((1 / b) * b) by A1, Lm3 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:109
for b, a being complex number st b <> 0 holds
a = (a * (1 / b)) * b
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * (1 / b)) * b )
assume A1: b <> 0 ; ::_thesis: a = (a * (1 / b)) * b
a = a * 1
.= a * ((1 / b) * b) by A1, Lm3 ;
hence  a = (a * (1 / b)) * b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:110
for b, a being complex number st b <> 0 holds
a = a / (b * (1 / b))
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a / (b * (1 / b)) )
assume A1: b <> 0 ; ::_thesis: a = a / (b * (1 / b))
thus a = a / 1
.= a / (b * (1 / b)) by A1, Th106 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:111
for a, b being complex number st a <> 0 & b <> 0 holds
1 / (a * b) <> 0 ;

theorem :: XCMPLX_1:112
for a, b being complex number st a <> 0 & b <> 0 holds
(a / b) * (b / a) = 1
proof
let a, b be complex number ; ::_thesis: ( a <> 0 & b <> 0 implies (a / b) * (b / a) = 1 )
assume A1: ( a <> 0 & b <> 0 ) ; ::_thesis: (a / b) * (b / a) = 1
 b / a = (a / b) " by Lm7;
hence  (a / b) * (b / a) = 1 by A1, XCMPLX_0:def_7; ::_thesis: verum
end;

theorem Th113: :: XCMPLX_1:113
for b, a, c being complex number st b <> 0 holds
(a / b) + c = (a + (b * c)) / b
proof
let b, a, c be complex number ; ::_thesis: ( b <> 0 implies (a / b) + c = (a + (b * c)) / b )
assume A1: b <> 0 ; ::_thesis: (a / b) + c = (a + (b * c)) / b
(a / b) + c = (a / b) + (1 * c)
.= (a / b) + ((b * (b ")) * c) by A1, XCMPLX_0:def_7
.= (a / b) + ((b * c) * (b "))
.= (a / b) + ((c * b) / b) by XCMPLX_0:def_9
.= (a + (c * b)) / b by Th62 ;
hence  (a / b) + c = (a + (b * c)) / b ; ::_thesis: verum
end;

theorem Th114: :: XCMPLX_1:114
for c, a, b being complex number st c <> 0 holds
a + b = c * ((a / c) + (b / c))
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a + b = c * ((a / c) + (b / c)) )
assume A1: c <> 0 ; ::_thesis: a + b = c * ((a / c) + (b / c))
hence a + b = (c * (a / c)) + b by Lm3
.= (c * (a / c)) + (c * (b / c)) by A1, Lm3
.= c * ((a / c) + (b / c)) ;
::_thesis: verum
end;

theorem Th115: :: XCMPLX_1:115
for c, a, b being complex number st c <> 0 holds
a + b = ((a * c) + (b * c)) / c
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a + b = ((a * c) + (b * c)) / c )
assume A1: c <> 0 ; ::_thesis: a + b = ((a * c) + (b * c)) / c
hence a + b = ((a * c) / c) + b by Lm9
.= ((a * c) / c) + ((b * c) / c) by A1, Lm9
.= ((a * c) + (b * c)) / c by Th62 ;
::_thesis: verum
end;

theorem Th116: :: XCMPLX_1:116
for b, d, a, c being complex number st b <> 0 & d <> 0 holds
(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
proof
let b, d, a, c be complex number ; ::_thesis: ( b <> 0 & d <> 0 implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume A1: b <> 0 ; ::_thesis: ( not d <> 0 or (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume  d <> 0 ; ::_thesis: (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
hence (a / b) + (c / d) = ((a * d) / (b * d)) + (c / d) by Lm10
.= ((a * d) / (b * d)) + ((c * b) / (b * d)) by A1, Lm10
.= ((a * d) + (c * b)) / (b * d) by Th62 ;
::_thesis: verum
end;

theorem Th117: :: XCMPLX_1:117
for a, b being complex number st a <> 0 holds
a + b = a * (1 + (b / a))
proof
let a, b be complex number ; ::_thesis: ( a <> 0 implies a + b = a * (1 + (b / a)) )
assume A1: a <> 0 ; ::_thesis: a + b = a * (1 + (b / a))
hence a + b = a * ((a / a) + (b / a)) by Th114
.= a * (1 + (b / a)) by A1, Lm5 ;
::_thesis: verum
end;

theorem :: XCMPLX_1:118
for a, b being complex number holds (a / (2 * b)) + (a / (2 * b)) = a / b
proof
let a, b be complex number ; ::_thesis: (a / (2 * b)) + (a / (2 * b)) = a / b
thus (a / (2 * b)) + (a / (2 * b)) = (a + a) / (2 * b) by Th62
.= (2 * a) / (2 * b)
.= a / b by Lm10 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:119
for a, b being complex number holds ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = a / b
proof
let a, b be complex number ; ::_thesis: ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = a / b
thus ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = ((a + a) / (3 * b)) + (a / (3 * b)) by Th62
.= ((a + a) + a) / (3 * b) by Th62
.= (3 * a) / (3 * b)
.= a / b by Lm10 ; ::_thesis: verum
end;

Lm17:  for a, b being complex number holds - (a / b) = (- a) / b
proof
let a, b be complex number ; ::_thesis: - (a / b) = (- a) / b
thus  - (a / b) = - (a * (b ")) by XCMPLX_0:def_9
.= (- a) * (b ")
.= (- a) / b by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem Th120: :: XCMPLX_1:120
for a, c, b being complex number holds (a / c) - (b / c) = (a - b) / c
proof
let a, c, b be complex number ; ::_thesis: (a / c) - (b / c) = (a - b) / c
thus (a / c) - (b / c) = (a / c) + (- (b / c))
.= (a / c) + ((- b) / c) by Lm17
.= (a + (- b)) / c by Th62
.= (a - b) / c ; ::_thesis: verum
end;

theorem :: XCMPLX_1:121
for a being complex number holds a - (a / 2) = a / 2 ;

theorem :: XCMPLX_1:122
for a, b, c, d being complex number holds ((a - b) - c) / d = ((a / d) - (b / d)) - (c / d)
proof
let a, b, c, d be complex number ; ::_thesis: ((a - b) - c) / d = ((a / d) - (b / d)) - (c / d)
thus ((a - b) - c) / d = ((a - b) / d) - (c / d) by Th120
.= ((a / d) - (b / d)) - (c / d) by Th120 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:123
for b, d, a, e being complex number st b <> 0 & d <> 0 & b <> d & a / b = e / d holds
a / b = (a - e) / (b - d)
proof
let b, d, a, e be complex number ; ::_thesis: ( b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = (a - e) / (b - d) )
assume that
A1: b <> 0 and
A2: d <> 0 and
A3: b <> d and
A4: a / b = e / d ; ::_thesis: a / b = (a - e) / (b - d)
 a * d = e * b by A1, A2, A4, Th95;
then A5: a * (b - d) = (a - e) * b ;
 b - d <> 0 by A3;
hence  a / b = (a - e) / (b - d) by A1, A5, Th94; ::_thesis: verum
end;

theorem :: XCMPLX_1:124
for a, b, e, d being complex number holds ((a + b) - e) / d = ((a / d) + (b / d)) - (e / d)
proof
let a, b, e, d be complex number ; ::_thesis: ((a + b) - e) / d = ((a / d) + (b / d)) - (e / d)
thus ((a + b) - e) / d = ((a + b) / d) - (e / d) by Th120
.= ((a / d) + (b / d)) - (e / d) by Th62 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:125
for a, b, e, d being complex number holds ((a - b) + e) / d = ((a / d) - (b / d)) + (e / d)
proof
let a, b, e, d be complex number ; ::_thesis: ((a - b) + e) / d = ((a / d) - (b / d)) + (e / d)
thus ((a - b) + e) / d = ((a - b) / d) + (e / d) by Th62
.= ((a / d) - (b / d)) + (e / d) by Th120 ; ::_thesis: verum
end;

theorem Th126: :: XCMPLX_1:126
for b, a, e being complex number st b <> 0 holds
(a / b) - e = (a - (e * b)) / b
proof
let b, a, e be complex number ; ::_thesis: ( b <> 0 implies (a / b) - e = (a - (e * b)) / b )
assume A1: b <> 0 ; ::_thesis: (a / b) - e = (a - (e * b)) / b
thus (a / b) - e = (a / b) + (- e)
.= (a + ((- e) * b)) / b by A1, Th113
.= (a - (e * b)) / b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:127
for b, c, a being complex number st b <> 0 holds
c - (a / b) = ((c * b) - a) / b
proof
let b, c, a be complex number ; ::_thesis: ( b <> 0 implies c - (a / b) = ((c * b) - a) / b )
assume A1: b <> 0 ; ::_thesis: c - (a / b) = ((c * b) - a) / b
thus c - (a / b) = - ((a / b) - c)
.= - ((a - (c * b)) / b) by A1, Th126
.= (- (a - (c * b))) / b by Lm17
.= ((c * b) - a) / b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:128
for c, a, b being complex number st c <> 0 holds
a - b = c * ((a / c) - (b / c))
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a - b = c * ((a / c) - (b / c)) )
assume A1: c <> 0 ; ::_thesis: a - b = c * ((a / c) - (b / c))
hence a - b = (c * (a / c)) - b by Lm3
.= (c * (a / c)) - (c * (b / c)) by A1, Lm3
.= c * ((a / c) - (b / c)) ;
::_thesis: verum
end;

theorem :: XCMPLX_1:129
for c, a, b being complex number st c <> 0 holds
a - b = ((a * c) - (b * c)) / c
proof
let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a - b = ((a * c) - (b * c)) / c )
assume A1: c <> 0 ; ::_thesis: a - b = ((a * c) - (b * c)) / c
thus a - b = a + (- b)
.= ((a * c) + ((- b) * c)) / c by A1, Th115
.= ((a * c) - (b * c)) / c ; ::_thesis: verum
end;

theorem :: XCMPLX_1:130
for b, d, a, c being complex number st b <> 0 & d <> 0 holds
(a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)
proof
let b, d, a, c be complex number ; ::_thesis: ( b <> 0 & d <> 0 implies (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) )
assume A1: b <> 0 ; ::_thesis: ( not d <> 0 or (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) )
assume A2: d <> 0 ; ::_thesis: (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)
thus (a / b) - (c / d) = (a / b) + (- (c / d))
.= (a / b) + ((- c) / d) by Lm17
.= ((a * d) + ((- c) * b)) / (b * d) by A1, A2, Th116
.= ((a * d) - (c * b)) / (b * d) ; ::_thesis: verum
end;

theorem :: XCMPLX_1:131
for a, b being complex number st a <> 0 holds
a - b = a * (1 - (b / a))
proof
let a, b be complex number ; ::_thesis: ( a <> 0 implies a - b = a * (1 - (b / a)) )
assume A1: a <> 0 ; ::_thesis: a - b = a * (1 - (b / a))
thus a - b = a + (- b)
.= a * (1 + ((- b) / a)) by A1, Th117
.= a * (1 + (- (b / a))) by Lm17
.= a * (1 - (b / a)) ; ::_thesis: verum
end;

theorem :: XCMPLX_1:132
for a, c, b being complex number st a <> 0 holds
c = (((a * c) + b) - b) / a by Lm9;

theorem :: XCMPLX_1:133
for a, b being complex number st - a = - b holds
a = b ;

theorem :: XCMPLX_1:134
for a being complex number st - a = 0 holds
a = 0 ;

theorem :: XCMPLX_1:135
for a, b being complex number st a + (- b) = 0 holds
a = b ;

theorem :: XCMPLX_1:136
for a, b being complex number holds a = (a + b) + (- b) ;

theorem :: XCMPLX_1:137
for a, b being complex number holds a = a + (b + (- b)) ;

theorem :: XCMPLX_1:138
for a, b being complex number holds a = ((- b) + a) + b ;

theorem :: XCMPLX_1:139
for a, b being complex number holds - (a + b) = (- a) + (- b) ;

theorem :: XCMPLX_1:140
for a, b being complex number holds - ((- a) + b) = a + (- b) ;

theorem :: XCMPLX_1:141
for a, b being complex number holds a + b = - ((- a) + (- b)) ;

theorem :: XCMPLX_1:142
for a, b being complex number holds - (a - b) = b - a ;

theorem :: XCMPLX_1:143
for a, b being complex number holds (- a) - b = (- b) - a ;

theorem :: XCMPLX_1:144
for a, b being complex number holds a = (- b) - ((- a) - b) ;

theorem :: XCMPLX_1:145
for a, b, c being complex number holds ((- a) - b) - c = ((- a) - c) - b ;

theorem :: XCMPLX_1:146
for a, b, c being complex number holds ((- a) - b) - c = ((- b) - c) - a ;

theorem :: XCMPLX_1:147
for a, b, c being complex number holds ((- a) - b) - c = ((- c) - b) - a ;

theorem :: XCMPLX_1:148
for c, a, b being complex number holds (c - a) - (c - b) = - (a - b) ;

theorem :: XCMPLX_1:149
for a being complex number holds 0 - a = - a ;

theorem :: XCMPLX_1:150
for a, b being complex number holds a + b = a - (- b) ;

theorem :: XCMPLX_1:151
for a, b being complex number holds a = a - (b + (- b)) ;

theorem :: XCMPLX_1:152
for a, c, b being complex number st a - c = b + (- c) holds
a = b ;

theorem :: XCMPLX_1:153
for c, a, b being complex number st c - a = c + (- b) holds
a = b ;

theorem :: XCMPLX_1:154
for a, b, c being complex number holds (a + b) - c = ((- c) + a) + b ;

theorem :: XCMPLX_1:155
for a, b, c being complex number holds (a - b) + c = ((- b) + c) + a ;

theorem :: XCMPLX_1:156
for a, b, c being complex number holds a - ((- b) - c) = (a + b) + c ;

theorem :: XCMPLX_1:157
for a, b, c being complex number holds (a - b) - c = ((- b) - c) + a ;

theorem :: XCMPLX_1:158
for a, b, c being complex number holds (a - b) - c = ((- c) + a) - b ;

theorem :: XCMPLX_1:159
for a, b, c being complex number holds (a - b) - c = ((- c) - b) + a ;

theorem :: XCMPLX_1:160
for a, b being complex number holds - (a + b) = (- b) - a ;

theorem :: XCMPLX_1:161
for a, b being complex number holds - (a - b) = (- a) + b ;

theorem :: XCMPLX_1:162
for a, b being complex number holds - ((- a) + b) = a - b ;

theorem :: XCMPLX_1:163
for a, b being complex number holds a + b = - ((- a) - b) ;

theorem :: XCMPLX_1:164
for a, b, c being complex number holds ((- a) + b) - c = ((- c) + b) - a ;

theorem :: XCMPLX_1:165
for a, b, c being complex number holds ((- a) + b) - c = ((- c) - a) + b ;

theorem :: XCMPLX_1:166
for a, b, c being complex number holds - ((a + b) + c) = ((- a) - b) - c ;

theorem :: XCMPLX_1:167
for a, b, c being complex number holds - ((a + b) - c) = ((- a) - b) + c ;

theorem :: XCMPLX_1:168
for a, b, c being complex number holds - ((a - b) + c) = ((- a) + b) - c ;

theorem :: XCMPLX_1:169
for a, b, c being complex number holds - ((a - b) - c) = ((- a) + b) + c ;

theorem :: XCMPLX_1:170
for a, b, c being complex number holds - (((- a) + b) + c) = (a - b) - c ;

theorem :: XCMPLX_1:171
for a, b, c being complex number holds - (((- a) + b) - c) = (a - b) + c ;

theorem :: XCMPLX_1:172
for a, b, c being complex number holds - (((- a) - b) + c) = (a + b) - c ;

theorem :: XCMPLX_1:173
for a, b, c being complex number holds - (((- a) - b) - c) = (a + b) + c ;

theorem :: XCMPLX_1:174
for a, b being complex number holds (- a) * b = - (a * b) ;

theorem :: XCMPLX_1:175
for a, b being complex number holds (- a) * b = a * (- b) ;

theorem :: XCMPLX_1:176
for a, b being complex number holds (- a) * (- b) = a * b ;

theorem :: XCMPLX_1:177
for a, b being complex number holds - (a * (- b)) = a * b ;

theorem :: XCMPLX_1:178
for a, b being complex number holds - ((- a) * b) = a * b ;

theorem :: XCMPLX_1:179
for a being complex number holds (- 1) * a = - a ;

theorem :: XCMPLX_1:180
for a being complex number holds (- a) * (- 1) = a ;

theorem Th181: :: XCMPLX_1:181
for b, a being complex number st b <> 0 & a * b = - b holds
a = - 1
proof
let b, a be complex number ; ::_thesis: ( b <> 0 & a * b = - b implies a = - 1 )
assume that
A1: b <> 0 and
A2: a * b = - b ; ::_thesis: a = - 1
 a * (b * (b ")) = (- b) * (b ") by A2, Th4;
then  a * 1 = (- b) * (b ") by A1, XCMPLX_0:def_7;
hence a = - (b * (b "))
.= - 1 by A1, XCMPLX_0:def_7 ;
::_thesis: verum
end;

theorem Th182: :: XCMPLX_1:182
for a being complex number holds
( not a * a = 1 or a = 1 or a = - 1 )
proof
let a be complex number ; ::_thesis: ( not a * a = 1 or a = 1 or a = - 1 )
assume  a * a = 1 ; ::_thesis: ( a = 1 or a = - 1 )
then  (a - 1) * (a + 1) = 0 ;
then  ( a - 1 = 0 or a + 1 = 0 ) ;
hence  ( a = 1 or a = - 1 ) ; ::_thesis: verum
end;

theorem :: XCMPLX_1:183
for a being complex number holds (- a) + (2 * a) = a ;

theorem :: XCMPLX_1:184
for a, b, c being complex number holds (a - b) * c = (b - a) * (- c) ;

theorem :: XCMPLX_1:185
for a, b, c being complex number holds (a - b) * c = - ((b - a) * c) ;

theorem :: XCMPLX_1:186
for a being complex number holds a - (2 * a) = - a ;

theorem :: XCMPLX_1:187
for a, b being complex number holds - (a / b) = (- a) / b by Lm17;

theorem Th188: :: XCMPLX_1:188
for a, b being complex number holds a / (- b) = - (a / b)
proof
let a, b be complex number ; ::_thesis: a / (- b) = - (a / b)
 a / (- b) = (a * (- 1)) / ((- b) * (- 1)) by Lm10;
then a / (- b) = (- a) / ((- (- b)) * 1)
.= - (a / b) by Lm17 ;
hence  a / (- b) = - (a / b) ; ::_thesis: verum
end;

theorem :: XCMPLX_1:189
for a, b being complex number holds - (a / (- b)) = a / b
proof
let a, b be complex number ; ::_thesis: - (a / (- b)) = a / b
thus  - (a / (- b)) = - (- (a / b)) by Th188
.= a / b ; ::_thesis: verum
end;

theorem Th190: :: XCMPLX_1:190
for a, b being complex number holds - ((- a) / b) = a / b
proof
let a, b be complex number ; ::_thesis: - ((- a) / b) = a / b
thus  - ((- a) / b) = - (- (a / b)) by Lm17
.= a / b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:191
for a, b being complex number holds (- a) / (- b) = a / b
proof
let a, b be complex number ; ::_thesis: (- a) / (- b) = a / b
 - ((- a) / b) = a / b by Th190;
hence  (- a) / (- b) = a / b by Th188; ::_thesis: verum
end;

theorem :: XCMPLX_1:192
for a, b being complex number holds (- a) / b = a / (- b)
proof
let a, b be complex number ; ::_thesis: (- a) / b = a / (- b)
thus (- a) / b = - (a / b) by Lm17
.= a / (- b) by Th188 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:193
for a being complex number holds - a = a / (- 1) ;

theorem :: XCMPLX_1:194
for a being complex number holds a = (- a) / (- 1) ;

theorem :: XCMPLX_1:195
for a, b being complex number st a / b = - 1 holds
( a = - b & b = - a )
proof
let a, b be complex number ; ::_thesis: ( a / b = - 1 implies ( a = - b & b = - a ) )
assume A1: a / b = - 1 ; ::_thesis: ( a = - b & b = - a )
then  b <> 0 by Th49;
then  a = (- 1) * b by A1, Lm3;
hence  ( a = - b & b = - a ) ; ::_thesis: verum
end;

theorem :: XCMPLX_1:196
for b, a being complex number st b <> 0 & b / a = - b holds
a = - 1
proof
let b, a be complex number ; ::_thesis: ( b <> 0 & b / a = - b implies a = - 1 )
assume that
A1: b <> 0 and
A2: b / a = - b ; ::_thesis: a = - 1
 a <> 0 by A1, A2, Th49;
then  b = (- b) * a by A2, Lm3;
then  b = - (b * a) ;
hence  a = - 1 by A1, A2, Th181; ::_thesis: verum
end;

theorem :: XCMPLX_1:197
for a being complex number st a <> 0 holds
(- a) / a = - 1
proof
let a be complex number ; ::_thesis: ( a <> 0 implies (- a) / a = - 1 )
assume A1: a <> 0 ; ::_thesis: (- a) / a = - 1
thus (- a) / a = - (a / a) by Lm17
.= - 1 by A1, Lm5 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:198
for a being complex number st a <> 0 holds
a / (- a) = - 1
proof
let a be complex number ; ::_thesis: ( a <> 0 implies a / (- a) = - 1 )
assume A1: a <> 0 ; ::_thesis: a / (- a) = - 1
thus a / (- a) = - (a / a) by Th188
.= - 1 by A1, Lm5 ; ::_thesis: verum
end;

Lm18:  for a being complex number st a <> 0 & a = a " & not a = 1 holds
a = - 1
proof
let a be complex number ; ::_thesis: ( a <> 0 & a = a " & not a = 1 implies a = - 1 )
assume A1: a <> 0 ; ::_thesis: ( not a = a " or a = 1 or a = - 1 )
assume  a = a " ; ::_thesis: ( a = 1 or a = - 1 )
then  a * a = 1 by A1, XCMPLX_0:def_7;
hence  ( a = 1 or a = - 1 ) by Th182; ::_thesis: verum
end;

theorem :: XCMPLX_1:199
for a being complex number st a <> 0 & a = 1 / a & not a = 1 holds
a = - 1
proof
let a be complex number ; ::_thesis: ( a <> 0 & a = 1 / a & not a = 1 implies a = - 1 )
assume  a <> 0 ; ::_thesis: ( not a = 1 / a or a = 1 or a = - 1 )
then  ( not a = a " or a = 1 or a = - 1 ) by Lm18;
hence  ( not a = 1 / a or a = 1 or a = - 1 ) by Lm4; ::_thesis: verum
end;

theorem :: XCMPLX_1:200
for b, d, a, e being complex number st b <> 0 & d <> 0 & b <> - d & a / b = e / d holds
a / b = (a + e) / (b + d)
proof
let b, d, a, e be complex number ; ::_thesis: ( b <> 0 & d <> 0 & b <> - d & a / b = e / d implies a / b = (a + e) / (b + d) )
assume that
A1: b <> 0 and
A2: d <> 0 and
A3: b <> - d and
A4: a / b = e / d ; ::_thesis: a / b = (a + e) / (b + d)
 a * d = e * b by A1, A2, A4, Th95;
then A5: a * (b + d) = (a + e) * b ;
 b + d <> 0 by A3;
hence  a / b = (a + e) / (b + d) by A1, A5, Th94; ::_thesis: verum
end;

theorem :: XCMPLX_1:201
for a, b being complex number st a " = b " holds
a = b by Lm12;

theorem :: XCMPLX_1:202
0 " = 0 ;

theorem :: XCMPLX_1:203
for b, a being complex number st b <> 0 holds
a = (a * b) * (b ")
proof
let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * b) * (b ") )
A1: a * (b * (b ")) = (a * b) * (b ") ;
assume  b <> 0 ; ::_thesis: a = (a * b) * (b ")
then  a * 1 = (a * b) * (b ") by A1, XCMPLX_0:def_7;
hence  a = (a * b) * (b ") ; ::_thesis: verum
end;

theorem :: XCMPLX_1:204
for a, b being complex number holds (a ") * (b ") = (a * b) " by Lm1;

theorem :: XCMPLX_1:205
for a, b being complex number holds (a * (b ")) " = (a ") * b by Lm11;

theorem :: XCMPLX_1:206
for a, b being complex number holds ((a ") * (b ")) " = a * b
proof
let a, b be complex number ; ::_thesis: ((a ") * (b ")) " = a * b
thus ((a ") * (b ")) " = ((a ") ") * ((b ") ") by Lm1
.= a * b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:207
for a, b being complex number st a <> 0 & b <> 0 holds
a * (b ") <> 0 ;

theorem :: XCMPLX_1:208
for a, b being complex number st a <> 0 & b <> 0 holds
(a ") * (b ") <> 0 ;

theorem :: XCMPLX_1:209
for a, b being complex number st a * (b ") = 1 holds
a = b
proof
let a, b be complex number ; ::_thesis: ( a * (b ") = 1 implies a = b )
assume  a * (b ") = 1 ; ::_thesis: a = b
then  a / b = 1 by XCMPLX_0:def_9;
hence  a = b by Th58; ::_thesis: verum
end;

theorem :: XCMPLX_1:210
for a, b being complex number st a * b = 1 holds
a = b "
proof
let a, b be complex number ; ::_thesis: ( a * b = 1 implies a = b " )
assume A1: a * b = 1 ; ::_thesis: a = b "
then  b <> 0 ;
hence  a = b " by A1, XCMPLX_0:def_7; ::_thesis: verum
end;

theorem Th211: :: XCMPLX_1:211
for a, b being complex number st a <> 0 & b <> 0 holds
(a ") + (b ") = (a + b) * ((a * b) ")
proof
let a, b be complex number ; ::_thesis: ( a <> 0 & b <> 0 implies (a ") + (b ") = (a + b) * ((a * b) ") )
assume that
A1: a <> 0 and
A2: b <> 0 ; ::_thesis: (a ") + (b ") = (a + b) * ((a * b) ")
 b " = (b ") * 1 ;
then  b " = (b ") * ((a ") * a) by A1, XCMPLX_0:def_7;
then  b " = ((a ") * (b ")) * a ;
then A3: b " = ((a * b) ") * a by Lm1;
 a " = (a ") * 1 ;
then  a " = (a ") * ((b ") * b) by A2, XCMPLX_0:def_7;
then  a " = ((a ") * (b ")) * b ;
then  a " = ((a * b) ") * b by Lm1;
hence  (a ") + (b ") = (a + b) * ((a * b) ") by A3; ::_thesis: verum
end;

Lm19:  for a being complex number holds (- a) " = - (a ")
proof
let a be complex number ; ::_thesis: (- a) " = - (a ")
thus (- a) " = 1 / (- a) by Lm4
.= - (1 / a) by Th188
.= - (a ") by Lm4 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:212
for a, b being complex number st a <> 0 & b <> 0 holds
(a ") - (b ") = (b - a) * ((a * b) ")
proof
let a, b be complex number ; ::_thesis: ( a <> 0 & b <> 0 implies (a ") - (b ") = (b - a) * ((a * b) ") )
assume A1: ( a <> 0 & b <> 0 ) ; ::_thesis: (a ") - (b ") = (b - a) * ((a * b) ")
thus (a ") - (b ") = (a ") + (- (b "))
.= (a ") + ((- b) ") by Lm19
.= (a + (- b)) * ((a * (- b)) ") by A1, Th211
.= (a + (- b)) * ((- (a * b)) ")
.= (a + (- b)) * (- ((a * b) ")) by Lm19
.= (b - a) * ((a * b) ") ; ::_thesis: verum
end;

theorem :: XCMPLX_1:213
for a, b being complex number holds (a / b) " = b / a by Lm7;

theorem :: XCMPLX_1:214
for a, b being complex number holds (a ") / (b ") = b / a
proof
let a, b be complex number ; ::_thesis: (a ") / (b ") = b / a
thus (a ") / (b ") = (a ") * ((b ") ") by XCMPLX_0:def_9
.= b / a by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:215
for a being complex number holds 1 / a = a " by Lm4;

theorem :: XCMPLX_1:216
for a being complex number holds 1 / (a ") = a by Lm16;

theorem :: XCMPLX_1:217
for a being complex number holds (1 / a) " = a
proof
let a be complex number ; ::_thesis: (1 / a) " = a
 ( 1 / a = a " implies (1 / a) " = a ) ;
hence  (1 / a) " = a by Lm4; ::_thesis: verum
end;

theorem :: XCMPLX_1:218
for a, b being complex number st 1 / a = b " holds
a = b
proof
let a, b be complex number ; ::_thesis: ( 1 / a = b " implies a = b )
 ( 1 / a = 1 / b implies a = b ) by Th59;
hence  ( 1 / a = b " implies a = b ) by Lm4; ::_thesis: verum
end;

theorem :: XCMPLX_1:219
for a, b being complex number holds a / (b ") = a * b
proof
let a, b be complex number ; ::_thesis: a / (b ") = a * b
thus a / (b ") = a * ((b ") ") by XCMPLX_0:def_9
.= a * b ; ::_thesis: verum
end;

theorem :: XCMPLX_1:220
for a, c, b being complex number holds (a ") * (c / b) = c / (a * b)
proof
let a, c, b be complex number ; ::_thesis: (a ") * (c / b) = c / (a * b)
thus (a ") * (c / b) = (a ") * (c * (b ")) by XCMPLX_0:def_9
.= c * ((a ") * (b "))
.= c * ((a * b) ") by Lm1
.= c / (a * b) by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:221
for a, b being complex number holds (a ") / b = (a * b) "
proof
let a, b be complex number ; ::_thesis: (a ") / b = (a * b) "
thus (a ") / b = (a ") * (b ") by XCMPLX_0:def_9
.= (a * b) " by Lm1 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:222
for a being complex number holds (- a) " = - (a ") by Lm19;

theorem :: XCMPLX_1:223
for a being complex number st a <> 0 & a = a " & not a = 1 holds
a = - 1 by Lm18;

begin

theorem :: XCMPLX_1:224
for a, b, c being complex number holds ((a + b) + c) - b = a + c ;

theorem :: XCMPLX_1:225
for a, b, c being complex number holds ((a - b) + c) + b = a + c ;

theorem :: XCMPLX_1:226
for a, b, c being complex number holds ((a + b) - c) - b = a - c ;

theorem :: XCMPLX_1:227
for a, b, c being complex number holds ((a - b) - c) + b = a - c ;

theorem :: XCMPLX_1:228
for a, b being complex number holds (a - a) - b = - b ;

theorem :: XCMPLX_1:229
for a, b being complex number holds ((- a) + a) - b = - b ;

theorem :: XCMPLX_1:230
for a, b being complex number holds (a - b) - a = - b ;

theorem :: XCMPLX_1:231
for a, b being complex number holds ((- a) - b) + a = - b ;

begin

theorem :: XCMPLX_1:232
for a, b being complex number st b <> 0 holds
ex e being complex number st a = b / e
proof
let a, b be complex number ; ::_thesis: ( b <> 0 implies ex e being complex number st a = b / e )
assume A1: b <> 0 ; ::_thesis: ex e being complex number st a = b / e
percases ( a = 0 or a <> 0 ) ;
supposeA2: a = 0 ; ::_thesis: ex e being complex number st a = b / e
take  0 ; ::_thesis: a = b / 0
 b / 0 = b * (0 ") by XCMPLX_0:def_9;
hence  a = b / 0 by A2; ::_thesis: verum
end;
supposeA3: a <> 0 ; ::_thesis: ex e being complex number st a = b / e
take e = b / a; ::_thesis: a = b / e
thus a = a * 1
.= a * (e * (e ")) by A1, A3, XCMPLX_0:def_7
.= (a * e) * (e ")
.= (a * ((a ") * b)) * (e ") by XCMPLX_0:def_9
.= ((a * (a ")) * b) * (e ")
.= (1 * b) * (e ") by A3, XCMPLX_0:def_7
.= b / e by XCMPLX_0:def_9 ; ::_thesis: verum
end;
end;
end;

theorem :: XCMPLX_1:233
for a, b, c, d, e being complex number holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
proof
let a, b, c, d, e be complex number ; ::_thesis: a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
thus a / ((b * c) * (d / e)) = a / ((b * c) * (d * (e "))) by XCMPLX_0:def_9
.= a / (c * ((b * d) * (e ")))
.= a / (c * ((b * d) / e)) by XCMPLX_0:def_9
.= a / ((b * d) / (e / c)) by Th81
.= (e / c) * (a / (b * d)) by Th81 ; ::_thesis: verum
end;

theorem :: XCMPLX_1:234
for d, c, b, a being complex number holds (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)
proof
let d, c, b, a be complex number ; ::_thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)
percases ( b = 0 or b <> 0 ) ;
supposeA1: b = 0 ; ::_thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)
A2: a / b = a * (b ") by XCMPLX_0:def_9
.= a * 0 by A1 ;
thus (((d - c) / b) * a) + c = (((d - c) * (b ")) * a) + c by XCMPLX_0:def_9
.= (((d - c) * 0) * a) + c by A1
.= ((1 - (a / b)) * c) + ((a / b) * d) by A2 ; ::_thesis: verum
end;
supposeA3: b <> 0 ; ::_thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)
(((d - c) / b) * a) + c = (((d - c) / b) * a) + (c * 1)
.= (((d - c) / b) * a) + (c * (b / b)) by A3, Lm5
.= (((d - c) / b) * a) + ((c * b) / b) by Lm8
.= (((d - c) * a) / b) + ((c * b) / b) by Lm8
.= (((d - c) * a) + (c * b)) / b by Th62
.= (((b - a) * c) + (a * d)) / b
.= (((b - a) * c) / b) + ((a * d) / b) by Th62
.= (((b - a) * c) / b) + ((a / b) * d) by Lm8
.= (((b - a) / b) * c) + ((a / b) * d) by Lm8
.= (((b / b) - (a / b)) * c) + ((a / b) * d) by Th120
.= ((1 - (a / b)) * c) + ((a / b) * d) by A3, Lm5 ;
hence  (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) ; ::_thesis: verum
end;
end;
end;

theorem :: XCMPLX_1:235
for a, b, c being complex number st a <> 0 holds
(a * b) + c = a * (b + (c / a))
proof
let a, b, c be complex number ; ::_thesis: ( a <> 0 implies (a * b) + c = a * (b + (c / a)) )
assume  a <> 0 ; ::_thesis: (a * b) + c = a * (b + (c / a))
hence (a * b) + c = (a * b) + (a * (c / a)) by Lm3
.= a * (b + (c / a)) ;
::_thesis: verum
end;