:: MATHMORP semantic presentation

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be Subset of (TOP-REAL c₁);
func c₃ + c₂ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 1
{ (b₁ + a₂) where B is Point of (TOP-REAL a₁) : b₁ in a₃ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines + MATHMORP:def 1 :

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
func c₂ ! -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 2
{ (- b₁) where B is Point of (TOP-REAL a₁) : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def2 defines ! MATHMORP:def 2 :

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func c₂ (-) c₃ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 3
{ b₁ where B is Point of (TOP-REAL a₁) : a₃ + b₁ c= a₂ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines (-) MATHMORP:def 3 :

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func c₂ (+) c₃ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 4
{ (b₁ + b₂) where B is Point of (TOP-REAL a₁), B is Point of (TOP-REAL a₁) : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def4 defines (+) MATHMORP:def 4 :

theorem Th1: :: MATHMORP:1

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds (b₂ ! ) ! = b₂

proof end;

theorem Th2: :: MATHMORP:2

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds {(0.REAL b₁)} + b₂ = {b₂}

proof end;

theorem Th3: :: MATHMORP:3

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) st b₂ c= b₃ holds
b₂ + b₄ c= b₃ + b₄

proof end;

theorem Th4: :: MATHMORP:4

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being Subset of (TOP-REAL b₁) st b₃ = {} holds
b₃ + b₂ = {}

proof end;

theorem Th5: :: MATHMORP:5

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds b₂ (-) {(0.REAL b₁)} = b₂

proof end;

Lemma5: for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds {b₂} + b₃ = {b₃} + b₂

proof end;

theorem Th6: :: MATHMORP:6

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds b₂ (+) {(0.REAL b₁)} = b₂

proof end;

theorem Th7: :: MATHMORP:7

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁) holds b₂ (+) {b₃} = b₂ + b₃

proof end;

theorem Th8: :: MATHMORP:8

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₃ = {} holds
b₂ (-) b₃ = REAL b₁

proof end;

theorem Th9: :: MATHMORP:9

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ c= b₃ holds
( b₂ (-) b₄ c= b₃ (-) b₄ & b₂ (+) b₄ c= b₃ (+) b₄ )

proof end;

theorem Th10: :: MATHMORP:10

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ c= b₃ holds
( b₄ (-) b₃ c= b₄ (-) b₂ & b₄ (+) b₂ c= b₄ (+) b₃ )

proof end;

theorem Th11: :: MATHMORP:11

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st 0.REAL b₁ in b₂ holds
( b₃ (-) b₂ c= b₃ & b₃ c= b₃ (+) b₂ )

proof end;

theorem Th12: :: MATHMORP:12

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds b₂ (+) b₃ = b₃ (+) b₂

proof end;

theorem Th13: :: MATHMORP:13

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄, b₅ being Point of (TOP-REAL b₁) holds
( b₂ + b₄ c= b₃ + b₅ iff b₂ + (b₄ - b₅) c= b₃ )

proof end;

theorem Th14: :: MATHMORP:14

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds (b₂ + b₄) (-) b₃ = (b₂ (-) b₃) + b₄

proof end;

theorem Th15: :: MATHMORP:15

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds (b₂ + b₄) (+) b₃ = (b₂ (+) b₃) + b₄

proof end;

theorem Th16: :: MATHMORP:16

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th17: :: MATHMORP:17

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds b₂ (-) (b₃ + b₄) = (b₂ (-) b₃) + (- b₄)

proof end;

theorem Th18: :: MATHMORP:18

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds b₂ (+) (b₃ + b₄) = (b₂ (+) b₃) + b₄

proof end;

theorem Th19: :: MATHMORP:19

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) st b₄ in b₂ holds
b₃ + b₄ c= b₃ (+) b₂

proof end;

theorem Th20: :: MATHMORP:20

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds b₂ c= (b₂ (+) b₃) (-) b₃

proof end;

theorem Th21: :: MATHMORP:21

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds b₂ + (0.REAL b₁) = b₂

proof end;

theorem Th22: :: MATHMORP:22

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁) holds b₂ (-) {b₃} = b₂ + (- b₃)

proof end;

Lemma18: for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds (b₂ (-) b₃) (+) b₃ c= b₂

proof end;

theorem Th23: :: MATHMORP:23

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (-) (b₃ (+) b₄) = (b₂ (-) b₃) (-) b₄

proof end;

theorem Th24: :: MATHMORP:24

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (-) (b₃ (+) b₄) = (b₂ (-) b₄) (-) b₃

proof end;

theorem Th25: :: MATHMORP:25

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (+) (b₃ (-) b₄) c= (b₂ (+) b₃) (-) b₄

proof end;

theorem Th26: :: MATHMORP:26

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (+) (b₃ (+) b₄) = (b₂ (+) b₃) (+) b₄

proof end;

theorem Th27: :: MATHMORP:27

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds (b₂ \/ b₃) + b₄ = (b₂ + b₄) \/ (b₃ + b₄)

proof end;

theorem Th28: :: MATHMORP:28

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds (b₂ /\ b₃) + b₄ = (b₂ + b₄) /\ (b₃ + b₄)

proof end;

theorem Th29: :: MATHMORP:29

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (-) (b₃ \/ b₄) = (b₂ (-) b₃) /\ (b₂ (-) b₄)

proof end;

theorem Th30: :: MATHMORP:30

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (+) (b₃ \/ b₄) = (b₂ (+) b₃) \/ (b₂ (+) b₄)

proof end;

theorem Th31: :: MATHMORP:31

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds (b₂ (-) b₃) \/ (b₄ (-) b₃) c= (b₂ \/ b₄) (-) b₃

proof end;

theorem Th32: :: MATHMORP:32

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds (b₂ \/ b₃) (+) b₄ = (b₂ (+) b₄) \/ (b₃ (+) b₄)

proof end;

theorem Th33: :: MATHMORP:33

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds (b₂ /\ b₃) (-) b₄ = (b₂ (-) b₄) /\ (b₃ (-) b₄)

proof end;

theorem Th34: :: MATHMORP:34

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds (b₂ /\ b₃) (+) b₄ c= (b₂ (+) b₄) /\ (b₃ (+) b₄)

proof end;

theorem Th35: :: MATHMORP:35

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (+) (b₃ /\ b₄) c= (b₂ (+) b₃) /\ (b₂ (+) b₄)

proof end;

theorem Th36: :: MATHMORP:36

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds (b₂ (-) b₃) \/ (b₂ (-) b₄) c= b₂ (-) (b₃ /\ b₄)

proof end;

theorem Th37: :: MATHMORP:37

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds ((b₂ ` ) (-) b₃) ` = b₂ (+) (b₃ ! )

proof end;

theorem Th38: :: MATHMORP:38

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds (b₂ (-) b₃) ` = (b₂ ` ) (+) (b₃ ! )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func c₂ (O) c₃ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 5
(a₂ (-) a₃) (+) a₃;
coherence ;

end;

:: deftheorem Def5 defines (O) MATHMORP:def 5 :

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func c₂ (o) c₃ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 6
(a₂ (+) a₃) (-) a₃;
coherence ;

end;

:: deftheorem Def6 defines (o) MATHMORP:def 6 :

theorem Th39: :: MATHMORP:39

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds ((b₂ ` ) (O) (b₃ ! )) ` = b₂ (o) b₃

proof end;

theorem Th40: :: MATHMORP:40

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds ((b₂ ` ) (o) (b₃ ! )) ` = b₂ (O) b₃

proof end;

theorem Th41: :: MATHMORP:41

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( b₂ (O) b₃ c= b₂ & b₂ c= b₂ (o) b₃ )

proof end;

theorem Th42: :: MATHMORP:42

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds b₂ (O) b₂ = b₂

proof end;

theorem Th43: :: MATHMORP:43

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( (b₂ (O) b₃) (-) b₃ c= b₂ (-) b₃ & (b₂ (O) b₃) (+) b₃ c= b₂ (+) b₃ )

proof end;

theorem Th44: :: MATHMORP:44

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( b₂ (-) b₃ c= (b₂ (o) b₃) (-) b₃ & b₂ (+) b₃ c= (b₂ (o) b₃) (+) b₃ )

proof end;

theorem Th45: :: MATHMORP:45

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ c= b₃ holds
( b₂ (O) b₄ c= b₃ (O) b₄ & b₂ (o) b₄ c= b₃ (o) b₄ )

proof end;

theorem Th46: :: MATHMORP:46

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds (b₂ + b₄) (O) b₃ = (b₂ (O) b₃) + b₄

proof end;

theorem Th47: :: MATHMORP:47

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) holds (b₂ + b₄) (o) b₃ = (b₂ (o) b₃) + b₄

proof end;

theorem Th48: :: MATHMORP:48

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ c= b₃ holds
b₄ (O) b₃ c= (b₄ (-) b₂) (+) b₃

proof end;

theorem Th49: :: MATHMORP:49

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ c= b₃ holds
b₄ (o) b₂ c= (b₄ (+) b₃) (-) b₂

proof end;

theorem Th50: :: MATHMORP:50

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( b₂ (+) b₃ = (b₂ (o) b₃) (+) b₃ & b₂ (-) b₃ = (b₂ (O) b₃) (-) b₃ )

proof end;

theorem Th51: :: MATHMORP:51

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds
( b₂ (+) b₃ = (b₂ (+) b₃) (O) b₃ & b₂ (-) b₃ = (b₂ (-) b₃) (o) b₃ )

proof end;

theorem Th52: :: MATHMORP:52

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds (b₂ (O) b₃) (O) b₃ = b₂ (O) b₃

proof end;

theorem Th53: :: MATHMORP:53

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) holds (b₂ (o) b₃) (o) b₃ = b₂ (o) b₃ by Th50;

theorem Th54: :: MATHMORP:54

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (O) b₃ c= (b₂ \/ b₄) (O) b₃

proof end;

theorem Th55: :: MATHMORP:55

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ = b₂ (O) b₃ holds
b₄ (O) b₂ c= b₄ (O) b₃

proof end;

definition

let c₁ be real number ;
let c₂ be Nat;
let c₃ be Subset of (TOP-REAL c₂);
func c₁ (.) c₃ -> Subset of (TOP-REAL a₂) equals :: MATHMORP:def 7
{ (a₁ * b₁) where B is Point of (TOP-REAL a₂) : b₁ in a₃ } ;
coherence

proof end;

end;

:: deftheorem Def7 defines (.) MATHMORP:def 7 :

theorem Th56: :: MATHMORP:56

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ = {} holds
0 (.) b₂ = {}

proof end;

theorem Th57: :: MATHMORP:57

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁) holds 0 (.) b₂ = {(0.REAL b₁)}

proof end;

theorem Th58: :: MATHMORP:58

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds 1 (.) b₂ = b₂

proof end;

theorem Th59: :: MATHMORP:59

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds 2 (.) b₂ c= b₂ (+) b₂

proof end;

theorem Th60: :: MATHMORP:60

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being real number holds (b₃ * b₄) (.) b₂ = b₃ (.) (b₄ (.) b₂)

proof end;

theorem Th61: :: MATHMORP:61

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₂ c= b₃ holds
b₄ (.) b₂ c= b₄ (.) b₃

proof end;

theorem Th62: :: MATHMORP:62

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being real number holds b₄ (.) (b₂ + b₃) = (b₄ (.) b₂) + (b₄ * b₃)

proof end;

theorem Th63: :: MATHMORP:63

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number holds b₄ (.) (b₂ (+) b₃) = (b₄ (.) b₂) (+) (b₄ (.) b₃)

proof end;

theorem Th64: :: MATHMORP:64

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₄ <> 0 holds
b₄ (.) (b₂ (-) b₃) = (b₄ (.) b₂) (-) (b₄ (.) b₃)

proof end;

theorem Th65: :: MATHMORP:65

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₄ <> 0 holds
b₄ (.) (b₂ (O) b₃) = (b₄ (.) b₂) (O) (b₄ (.) b₃)

proof end;

theorem Th66: :: MATHMORP:66

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₄ <> 0 holds
b₄ (.) (b₂ (o) b₃) = (b₄ (.) b₂) (o) (b₄ (.) b₃)

proof end;

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Subset of (TOP-REAL c₁);
func c₂ (*) c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 8
(a₂ (-) a₃) /\ ((a₂ ` ) (-) a₄);
coherence ;

end;

:: deftheorem Def8 defines (*) MATHMORP:def 8 :

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Subset of (TOP-REAL c₁);
func c₂ (&) c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 9
a₂ \/ (a₂ (*) a₃,a₄);
coherence ;

end;

:: deftheorem Def9 defines (&) MATHMORP:def 9 :

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Subset of (TOP-REAL c₁);
func c₂ (@) c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: MATHMORP:def 10
a₂ \ (a₂ (*) a₃,a₄);
coherence ;

end;

:: deftheorem Def10 defines (@) MATHMORP:def 10 :

theorem Th67: :: MATHMORP:67

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ = {} holds
b₃ (*) b₂,b₄ = (b₃ ` ) (-) b₄

proof end;

theorem Th68: :: MATHMORP:68

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ = {} holds
b₃ (*) b₄,b₂ = b₃ (-) b₄

proof end;

theorem Th69: :: MATHMORP:69

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st 0.REAL b₁ in b₂ holds
b₃ (*) b₂,b₄ c= b₃

proof end;

theorem Th70: :: MATHMORP:70

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st 0.REAL b₁ in b₂ holds
(b₃ (*) b₄,b₂) /\ b₃ = {}

proof end;

theorem Th71: :: MATHMORP:71

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st 0.REAL b₁ in b₂ holds
b₃ (&) b₂,b₄ = b₃

proof end;

theorem Th72: :: MATHMORP:72

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) st 0.REAL b₁ in b₂ holds
b₃ (@) b₄,b₂ = b₃

proof end;

theorem Th73: :: MATHMORP:73

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (&) b₃,b₄ = ((b₂ ` ) (@) b₄,b₃) ` by SUBSET_1:33;

theorem Th74: :: MATHMORP:74

for b₁ being Nat
for b₂, b₃, b₄ being Subset of (TOP-REAL b₁) holds b₂ (@) b₃,b₄ = ((b₂ ` ) (&) b₄,b₃) `

proof end;

theorem Th75: :: MATHMORP:75

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) holds
( b₂ is convex iff for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅ being real number st 0 <= b₅ & b₅ <= 1 & b₃ in b₂ & b₄ in b₂ holds
(b₅ * b₃) + ((1 - b₅) * b₄) in b₂ )

proof end;

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
redefine attr a₂ is convex means :Def11: :: MATHMORP:def 11
for b₁, b₂ being Point of (TOP-REAL a₁)
for b₃ being real number st 0 <= b₃ & b₃ <= 1 & b₁ in a₂ & b₂ in a₂ holds
(b₃ * b₁) + ((1 - b₃) * b₂) in a₂;
compatibility by Th75;

end;

:: deftheorem Def11 defines convex MATHMORP:def 11 :

theorem Th76: :: MATHMORP:76

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ is convex holds
b₂ ! is convex

proof end;

theorem Th77: :: MATHMORP:77

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₂ is convex & b₃ is convex holds
( b₂ (+) b₃ is convex & b₂ (-) b₃ is convex )

proof end;

theorem Th78: :: MATHMORP:78

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₂ is convex & b₃ is convex holds
( b₂ (O) b₃ is convex & b₂ (o) b₃ is convex )

proof end;

theorem Th79: :: MATHMORP:79

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being real number st b₂ is convex & 0 < b₃ & 0 < b₄ holds
(b₄ + b₃) (.) b₂ = (b₄ (.) b₂) (+) (b₃ (.) b₂)

proof end;