:: VFUNCT_1 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
let c₃, c₄ be PartFunc of c₁,the carrier of c₂;
deffunc H₁( Element of c₁) -> Element of the carrier of c₂ = (c₃ /. a₁) + (c₄ /. a₁);
deffunc H₂( Element of c₁) -> Element of the carrier of c₂ = (c₃ /. a₁) - (c₄ /. a₁);
defpred S₁[ set ] means a₁ in (dom c₃) /\ (dom c₄);
set c₅ = (dom c₃) /\ (dom c₄);
func c₃ + c₄ -> PartFunc of a₁,the carrier of a₂ means :Def1: :: VFUNCT_1:def 1
( dom a₅ = (dom a₃) /\ (dom a₄) & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = (a₃ /. b₁) + (a₄ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

func c₃ - c₄ -> PartFunc of a₁,the carrier of a₂ means :Def2: :: VFUNCT_1:def 2
( dom a₅ = (dom a₃) /\ (dom a₄) & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = (a₃ /. b₁) - (a₄ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines + VFUNCT_1:def 1 :

:: deftheorem Def2 defines - VFUNCT_1:def 2 :

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁, REAL ;
let c₄ be PartFunc of c₁,the carrier of c₂;
deffunc H₁( Element of c₁) -> Element of the carrier of c₂ = (c₃ . a₁) * (c₄ /. a₁);
defpred S₁[ set ] means a₁ in (dom c₃) /\ (dom c₄);
set c₅ = (dom c₃) /\ (dom c₄);
func c₃ (#) c₄ -> PartFunc of a₁,the carrier of a₂ means :Def3: :: VFUNCT_1:def 3
( dom a₅ = (dom a₃) /\ (dom a₄) & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = (a₃ . b₁) * (a₄ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines (#) VFUNCT_1:def 3 :

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,the carrier of c₂;
let c₄ be Real;
deffunc H₁( Element of c₁) -> Element of the carrier of c₂ = c₄ * (c₃ /. a₁);
defpred S₁[ set ] means a₁ in dom c₃;
set c₅ = dom c₃;
func c₄ (#) c₃ -> PartFunc of a₁,the carrier of a₂ means :Def4: :: VFUNCT_1:def 4
( dom a₅ = dom a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = a₄ * (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines (#) VFUNCT_1:def 4 :

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,the carrier of c₂;
deffunc H₁( Element of c₁) -> Element of REAL = ||.(c₃ /. a₁).||;
deffunc H₂( Element of c₁) -> Element of the carrier of c₂ = - (c₃ /. a₁);
defpred S₁[ set ] means a₁ in dom c₃;
set c₄ = dom c₃;
func ||.c₃.|| -> PartFunc of a₁, REAL means :Def5: :: VFUNCT_1:def 5
( dom a₄ = dom a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = ||.(a₃ /. b₁).|| ) );
existence

proof end;

uniqueness

proof end;

func - c₃ -> PartFunc of a₁,the carrier of a₂ means :Def6: :: VFUNCT_1:def 6
( dom a₄ = dom a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ /. b₁ = - (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ||. VFUNCT_1:def 5 :

:: deftheorem Def6 defines - VFUNCT_1:def 6 :

theorem Th1: :: VFUNCT_1:1

canceled;

theorem Th2: :: VFUNCT_1:2

canceled;

theorem Th3: :: VFUNCT_1:3

canceled;

theorem Th4: :: VFUNCT_1:4

canceled;

theorem Th5: :: VFUNCT_1:5

canceled;

theorem Th6: :: VFUNCT_1:6

canceled;

theorem Th7: :: VFUNCT_1:7

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being PartFunc of b₁, REAL holds (dom (b₄ (#) b₃)) \ ((b₄ (#) b₃) " {(0. b₂)}) = ((dom b₄) \ (b₄ " {0})) /\ ((dom b₃) \ (b₃ " {(0. b₂)}))

proof end;

theorem Th8: :: VFUNCT_1:8

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds
( ||.b₃.|| " {0} = b₃ " {(0. b₂)} & (- b₃) " {(0. b₂)} = b₃ " {(0. b₂)} )

proof end;

theorem Th9: :: VFUNCT_1:9

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Real st b₄ <> 0 holds
(b₄ (#) b₃) " {(0. b₂)} = b₃ " {(0. b₂)}

proof end;

theorem Th10: :: VFUNCT_1:10

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

theorem Th11: :: VFUNCT_1:11

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds (b₃ + b₄) + b₅ = b₃ + (b₄ + b₅)

proof end;

theorem Th12: :: VFUNCT_1:12

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁, REAL
for b₅ being PartFunc of b₁,the carrier of b₂ holds (b₃ (#) b₄) (#) b₅ = b₃ (#) (b₄ (#) b₅)

proof end;

theorem Th13: :: VFUNCT_1:13

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being PartFunc of b₁, REAL holds (b₄ + b₅) (#) b₃ = (b₄ (#) b₃) + (b₅ (#) b₃)

proof end;

theorem Th14: :: VFUNCT_1:14

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being PartFunc of b₁, REAL holds b₅ (#) (b₃ + b₄) = (b₅ (#) b₃) + (b₅ (#) b₄)

proof end;

theorem Th15: :: VFUNCT_1:15

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Real
for b₅ being PartFunc of b₁, REAL holds b₄ (#) (b₅ (#) b₃) = (b₄ (#) b₅) (#) b₃

proof end;

theorem Th16: :: VFUNCT_1:16

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Real
for b₅ being PartFunc of b₁, REAL holds b₄ (#) (b₅ (#) b₃) = b₅ (#) (b₄ (#) b₃)

proof end;

theorem Th17: :: VFUNCT_1:17

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being PartFunc of b₁, REAL holds (b₄ - b₅) (#) b₃ = (b₄ (#) b₃) - (b₅ (#) b₃)

proof end;

theorem Th18: :: VFUNCT_1:18

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being PartFunc of b₁, REAL holds (b₅ (#) b₃) - (b₅ (#) b₄) = b₅ (#) (b₃ - b₄)

proof end;

theorem Th19: :: VFUNCT_1:19

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being Real holds b₅ (#) (b₃ + b₄) = (b₅ (#) b₃) + (b₅ (#) b₄)

proof end;

theorem Th20: :: VFUNCT_1:20

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being Real holds (b₄ * b₅) (#) b₃ = b₄ (#) (b₅ (#) b₃)

proof end;

theorem Th21: :: VFUNCT_1:21

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being Real holds b₅ (#) (b₃ - b₄) = (b₅ (#) b₃) - (b₅ (#) b₄)

proof end;

theorem Th22: :: VFUNCT_1:22

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ - b₄ = (- 1) (#) (b₄ - b₃)

proof end;

theorem Th23: :: VFUNCT_1:23

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds b₃ - (b₄ + b₅) = (b₃ - b₄) - b₅

proof end;

theorem Th24: :: VFUNCT_1:24

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds 1 (#) b₃ = b₃

proof end;

theorem Th25: :: VFUNCT_1:25

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds b₃ - (b₄ - b₅) = (b₃ - b₄) + b₅

proof end;

theorem Th26: :: VFUNCT_1:26

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds b₃ + (b₄ - b₅) = (b₃ + b₄) - b₅

proof end;

theorem Th27: :: VFUNCT_1:27

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being PartFunc of b₁, REAL holds ||.(b₄ (#) b₃).|| = (abs b₄) (#) ||.b₃.||

proof end;

theorem Th28: :: VFUNCT_1:28

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Real holds ||.(b₄ (#) b₃).|| = (abs b₄) (#) ||.b₃.||

proof end;

theorem Th29: :: VFUNCT_1:29

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds - b₃ = (- 1) (#) b₃

proof end;

theorem Th30: :: VFUNCT_1:30

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds - (- b₃) = b₃

proof end;

theorem Th31: :: VFUNCT_1:31

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ - b₄ = b₃ + (- b₄)

proof end;

theorem Th32: :: VFUNCT_1:32

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ - (- b₄) = b₃ + b₄

proof end;

theorem Th33: :: VFUNCT_1:33

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄, b₅ being PartFunc of b₂,the carrier of b₃ holds
( (b₄ + b₅) | b₁ = (b₄ | b₁) + (b₅ | b₁) & (b₄ + b₅) | b₁ = (b₄ | b₁) + b₅ & (b₄ + b₅) | b₁ = b₄ + (b₅ | b₁) )

proof end;

theorem Th34: :: VFUNCT_1:34

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃
for b₅ being PartFunc of b₂, REAL holds
( (b₅ (#) b₄) | b₁ = (b₅ | b₁) (#) (b₄ | b₁) & (b₅ (#) b₄) | b₁ = (b₅ | b₁) (#) b₄ & (b₅ (#) b₄) | b₁ = b₅ (#) (b₄ | b₁) )

proof end;

theorem Th35: :: VFUNCT_1:35

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ holds
( (- b₄) | b₁ = - (b₄ | b₁) & ||.b₄.|| | b₁ = ||.(b₄ | b₁).|| )

proof end;

theorem Th36: :: VFUNCT_1:36

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄, b₅ being PartFunc of b₂,the carrier of b₃ holds
( (b₄ - b₅) | b₁ = (b₄ | b₁) - (b₅ | b₁) & (b₄ - b₅) | b₁ = (b₄ | b₁) - b₅ & (b₄ - b₅) | b₁ = b₄ - (b₅ | b₁) )

proof end;

theorem Th37: :: VFUNCT_1:37

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃
for b₅ being Real holds (b₅ (#) b₄) | b₁ = b₅ (#) (b₄ | b₁)

proof end;

theorem Th38: :: VFUNCT_1:38

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds
( ( b₃ is total & b₄ is total implies b₃ + b₄ is total ) & ( b₃ + b₄ is total implies ( b₃ is total & b₄ is total ) ) & ( b₃ is total & b₄ is total implies b₃ - b₄ is total ) & ( b₃ - b₄ is total implies ( b₃ is total & b₄ is total ) ) )

proof end;

theorem Th39: :: VFUNCT_1:39

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being PartFunc of b₁, REAL holds
( ( b₄ is total & b₃ is total ) iff b₄ (#) b₃ is total )

proof end;

theorem Th40: :: VFUNCT_1:40

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Real holds
( b₃ is total iff b₄ (#) b₃ is total )

proof end;

theorem Th41: :: VFUNCT_1:41

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds
( b₃ is total iff - b₃ is total )

proof end;

theorem Th42: :: VFUNCT_1:42

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds
( b₃ is total iff ||.b₃.|| is total )

proof end;

theorem Th43: :: VFUNCT_1:43

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being RealNormSpace
for b₄, b₅ being PartFunc of b₁,the carrier of b₃ st b₄ is total & b₅ is total holds
( (b₄ + b₅) /. b₂ = (b₄ /. b₂) + (b₅ /. b₂) & (b₄ - b₅) /. b₂ = (b₄ /. b₂) - (b₅ /. b₂) )

proof end;

theorem Th44: :: VFUNCT_1:44

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being RealNormSpace
for b₄ being PartFunc of b₁,the carrier of b₃
for b₅ being PartFunc of b₁, REAL st b₅ is total & b₄ is total holds
(b₅ (#) b₄) /. b₂ = (b₅ . b₂) * (b₄ /. b₂)

proof end;

theorem Th45: :: VFUNCT_1:45

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being RealNormSpace
for b₄ being PartFunc of b₁,the carrier of b₃
for b₅ being Real st b₄ is total holds
(b₅ (#) b₄) /. b₂ = b₅ * (b₄ /. b₂)

proof end;

theorem Th46: :: VFUNCT_1:46

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being RealNormSpace
for b₄ being PartFunc of b₁,the carrier of b₃ st b₄ is total holds
( (- b₄) /. b₂ = - (b₄ /. b₂) & ||.b₄.|| . b₂ = ||.(b₄ /. b₂).|| )

proof end;

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,the carrier of c₂;
let c₄ be set ;
pred c₃ is_bounded_on c₄ means :Def7: :: VFUNCT_1:def 7
ex b₁ being Real st
for b₂ being Element of a₁ st b₂ in a₄ /\ (dom a₃) holds
||.(a₃ /. b₂).|| <= b₁;

end;

:: deftheorem Def7 defines is_bounded_on VFUNCT_1:def 7 :

theorem Th47: :: VFUNCT_1:47

canceled;

theorem Th48: :: VFUNCT_1:48

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅ being PartFunc of b₃,the carrier of b₄ st b₁ c= b₂ & b₅ is_bounded_on b₂ holds
b₅ is_bounded_on b₁

proof end;

theorem Th49: :: VFUNCT_1:49

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ st b₁ misses dom b₄ holds
b₄ is_bounded_on b₁

proof end;

theorem Th50: :: VFUNCT_1:50

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ holds 0 (#) b₄ is_bounded_on b₁

proof end;

theorem Th51: :: VFUNCT_1:51

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃
for b₅ being Real st b₄ is_bounded_on b₁ holds
b₅ (#) b₄ is_bounded_on b₁

proof end;

theorem Th52: :: VFUNCT_1:52

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ st b₄ is_bounded_on b₁ holds
( ||.b₄.|| is_bounded_on b₁ & - b₄ is_bounded_on b₁ )

proof end;

theorem Th53: :: VFUNCT_1:53

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,the carrier of b₄ st b₅ is_bounded_on b₁ & b₆ is_bounded_on b₂ holds
b₅ + b₆ is_bounded_on b₁ /\ b₂

proof end;

theorem Th54: :: VFUNCT_1:54

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅ being PartFunc of b₃,the carrier of b₄
for b₆ being PartFunc of b₃, REAL st b₆ is_bounded_on b₁ & b₅ is_bounded_on b₂ holds
b₆ (#) b₅ is_bounded_on b₁ /\ b₂

proof end;

theorem Th55: :: VFUNCT_1:55

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,the carrier of b₄ st b₅ is_bounded_on b₁ & b₆ is_bounded_on b₂ holds
b₅ - b₆ is_bounded_on b₁ /\ b₂

proof end;

theorem Th56: :: VFUNCT_1:56

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅ being PartFunc of b₃,the carrier of b₄ st b₅ is_bounded_on b₁ & b₅ is_bounded_on b₂ holds
b₅ is_bounded_on b₁ \/ b₂

proof end;

theorem Th57: :: VFUNCT_1:57

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,the carrier of b₄ st b₅ is_constant_on b₁ & b₆ is_constant_on b₂ holds
( b₅ + b₆ is_constant_on b₁ /\ b₂ & b₅ - b₆ is_constant_on b₁ /\ b₂ )

proof end;

theorem Th58: :: VFUNCT_1:58

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅ being PartFunc of b₃,the carrier of b₄
for b₆ being PartFunc of b₃, REAL st b₆ is_constant_on b₁ & b₅ is_constant_on b₂ holds
b₆ (#) b₅ is_constant_on b₁ /\ b₂

proof end;

theorem Th59: :: VFUNCT_1:59

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃
for b₅ being Real st b₄ is_constant_on b₁ holds
b₅ (#) b₄ is_constant_on b₁

proof end;

theorem Th60: :: VFUNCT_1:60

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ st b₄ is_constant_on b₁ holds
( ||.b₄.|| is_constant_on b₁ & - b₄ is_constant_on b₁ )

proof end;

theorem Th61: :: VFUNCT_1:61

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ st b₄ is_constant_on b₁ holds
b₄ is_bounded_on b₁

proof end;

theorem Th62: :: VFUNCT_1:62

for b₁ being set
for b₂ being non empty set
for b₃ being RealNormSpace
for b₄ being PartFunc of b₂,the carrier of b₃ st b₄ is_constant_on b₁ holds
( ( for b₅ being Real holds b₅ (#) b₄ is_bounded_on b₁ ) & - b₄ is_bounded_on b₁ & ||.b₄.|| is_bounded_on b₁ )

proof end;

theorem Th63: :: VFUNCT_1:63

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,the carrier of b₄ st b₅ is_bounded_on b₁ & b₆ is_constant_on b₂ holds
b₅ + b₆ is_bounded_on b₁ /\ b₂

proof end;

theorem Th64: :: VFUNCT_1:64

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,the carrier of b₄ st b₅ is_bounded_on b₁ & b₆ is_constant_on b₂ holds
( b₅ - b₆ is_bounded_on b₁ /\ b₂ & b₆ - b₅ is_bounded_on b₁ /\ b₂ )

proof end;