:: VFUNCT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let C be non empty set ;
let V be RealNormSpace;
let f1, f2 be PartFunc of C,the carrier of V;
deffunc H1( Element of C) -> Element of the carrier of V = (f1 /. $1) + (f2 /. $1);
deffunc H2( Element of C) -> Element of the carrier of V = (f1 /. $1) - (f2 /. $1);
defpred S1[ set ] means $1 in (dom f1) /\ (dom f2);
set X = (dom f1) /\ (dom f2);
func f1 + f2 -> PartFunc of C,the carrier of V means :Def1: :: VFUNCT_1:def 1
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds
it /. c = (f1 /. c) + (f2 /. c) ) );
existence
ex b1 being PartFunc of C,the carrier of V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) + (f2 /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,the carrier of V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) + (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f1 /. c) + (f2 /. c) ) holds
b1 = b2
proof end;
func f1 - f2 -> PartFunc of C,the carrier of V means :Def2: :: VFUNCT_1:def 2
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds
it /. c = (f1 /. c) - (f2 /. c) ) );
existence
ex b1 being PartFunc of C,the carrier of V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) - (f2 /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,the carrier of V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) - (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f1 /. c) - (f2 /. c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines + VFUNCT_1:def 1 :
for C being non empty set
for V being RealNormSpace
for f1, f2, b5 being PartFunc of C,the carrier of V holds
( b5 = f1 + f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b5 holds
b5 /. c = (f1 /. c) + (f2 /. c) ) ) );

:: deftheorem Def2 defines - VFUNCT_1:def 2 :
for C being non empty set
for V being RealNormSpace
for f1, f2, b5 being PartFunc of C,the carrier of V holds
( b5 = f1 - f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b5 holds
b5 /. c = (f1 /. c) - (f2 /. c) ) ) );

definition
let C be non empty set ;
let V be RealNormSpace;
let f1 be PartFunc of C, REAL ;
let f2 be PartFunc of C,the carrier of V;
deffunc H1( Element of C) -> Element of the carrier of V = (f1 . $1) * (f2 /. $1);
defpred S1[ set ] means $1 in (dom f1) /\ (dom f2);
set X = (dom f1) /\ (dom f2);
func f1 (#) f2 -> PartFunc of C,the carrier of V means :Def3: :: VFUNCT_1:def 3
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds
it /. c = (f1 . c) * (f2 /. c) ) );
existence
ex b1 being PartFunc of C,the carrier of V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 . c) * (f2 /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,the carrier of V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 . c) * (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f1 . c) * (f2 /. c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines (#) VFUNCT_1:def 3 :
for C being non empty set
for V being RealNormSpace
for f1 being PartFunc of C, REAL
for f2, b5 being PartFunc of C,the carrier of V holds
( b5 = f1 (#) f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b5 holds
b5 /. c = (f1 . c) * (f2 /. c) ) ) );

definition
let C be non empty set ;
let V be RealNormSpace;
let f be PartFunc of C,the carrier of V;
let r be Real;
deffunc H1( Element of C) -> Element of the carrier of V = r * (f /. $1);
defpred S1[ set ] means $1 in dom f;
set X = dom f;
func r (#) f -> PartFunc of C,the carrier of V means :Def4: :: VFUNCT_1:def 4
( dom it = dom f & ( for c being Element of C st c in dom it holds
it /. c = r * (f /. c) ) );
existence
ex b1 being PartFunc of C,the carrier of V st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = r * (f /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,the carrier of V st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = r * (f /. c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 /. c = r * (f /. c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines (#) VFUNCT_1:def 4 :
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real
for b5 being PartFunc of C,the carrier of V holds
( b5 = r (#) f iff ( dom b5 = dom f & ( for c being Element of C st c in dom b5 holds
b5 /. c = r * (f /. c) ) ) );

definition
let C be non empty set ;
let V be RealNormSpace;
let f be PartFunc of C,the carrier of V;
deffunc H1( Element of C) -> Element of REAL = ||.(f /. $1).||;
deffunc H2( Element of C) -> Element of the carrier of V = - (f /. $1);
defpred S1[ set ] means $1 in dom f;
set X = dom f;
func ||.f.|| -> PartFunc of C, REAL means :Def5: :: VFUNCT_1:def 5
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = ||.(f /. c).|| ) );
existence
ex b1 being PartFunc of C, REAL st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = ||.(f /. c).|| ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C, REAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = ||.(f /. c).|| ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 . c = ||.(f /. c).|| ) holds
b1 = b2
proof end;
func - f -> PartFunc of C,the carrier of V means :Def6: :: VFUNCT_1:def 6
( dom it = dom f & ( for c being Element of C st c in dom it holds
it /. c = - (f /. c) ) );
existence
ex b1 being PartFunc of C,the carrier of V st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = - (f /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,the carrier of V st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = - (f /. c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 /. c = - (f /. c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ||. VFUNCT_1:def 5 :
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for b4 being PartFunc of C, REAL holds
( b4 = ||.f.|| iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds
b4 . c = ||.(f /. c).|| ) ) );

:: deftheorem Def6 defines - VFUNCT_1:def 6 :
for C being non empty set
for V being RealNormSpace
for f, b4 being PartFunc of C,the carrier of V holds
( b4 = - f iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds
b4 /. c = - (f /. c) ) ) );

theorem :: VFUNCT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
proof end;

theorem :: VFUNCT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
proof end;

theorem :: VFUNCT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
proof end;

theorem :: VFUNCT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds f1 + f2 = f2 + f1
proof end;

theorem :: VFUNCT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,the carrier of V holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof end;

theorem :: VFUNCT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C, REAL
for f3 being PartFunc of C,the carrier of V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof end;

theorem :: VFUNCT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f3 being PartFunc of C,the carrier of V
for f1, f2 being PartFunc of C, REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof end;

theorem :: VFUNCT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V
for f3 being PartFunc of C, REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
proof end;

theorem :: VFUNCT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for r being Real
for f1 being PartFunc of C, REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
proof end;

theorem :: VFUNCT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for r being Real
for f1 being PartFunc of C, REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
proof end;

theorem :: VFUNCT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f3 being PartFunc of C,the carrier of V
for f1, f2 being PartFunc of C, REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof end;

theorem :: VFUNCT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V
for f3 being PartFunc of C, REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
proof end;

theorem :: VFUNCT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V
for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
proof end;

theorem Th20: :: VFUNCT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
proof end;

theorem :: VFUNCT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V
for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
proof end;

theorem :: VFUNCT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds f1 - f2 = (- 1) (#) (f2 - f1)
proof end;

theorem :: VFUNCT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,the carrier of V holds f1 - (f2 + f3) = (f1 - f2) - f3
proof end;

theorem Th24: :: VFUNCT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds 1 (#) f = f
proof end;

theorem :: VFUNCT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,the carrier of V holds f1 - (f2 - f3) = (f1 - f2) + f3
proof end;

theorem :: VFUNCT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,the carrier of V holds f1 + (f2 - f3) = (f1 + f2) - f3
proof end;

theorem :: VFUNCT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
proof end;

theorem :: VFUNCT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
proof end;

theorem Th29: :: VFUNCT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds - f = (- 1) (#) f
proof end;

theorem Th30: :: VFUNCT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds - (- f) = f
proof end;

theorem Th31: :: VFUNCT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds f1 - f2 = f1 + (- f2)
proof end;

theorem :: VFUNCT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds f1 - (- f2) = f1 + f2
proof end;

theorem Th33: :: VFUNCT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof end;

theorem :: VFUNCT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
proof end;

theorem Th35: :: VFUNCT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
proof end;

theorem :: VFUNCT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof end;

theorem :: VFUNCT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real holds (r (#) f) | X = r (#) (f | X)
proof end;

theorem Th38: :: VFUNCT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) )
proof end;

theorem Th39: :: VFUNCT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
proof end;

theorem Th40: :: VFUNCT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real holds
( f is total iff r (#) f is total )
proof end;

theorem Th41: :: VFUNCT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds
( f is total iff - f is total )
proof end;

theorem Th42: :: VFUNCT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds
( f is total iff ||.f.|| is total )
proof end;

theorem :: VFUNCT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
proof end;

theorem :: VFUNCT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL st f1 is total & f2 is total holds
(f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
proof end;

theorem :: VFUNCT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
proof end;

theorem :: VFUNCT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
proof end;

definition
let C be non empty set ;
let V be RealNormSpace;
let f be PartFunc of C,the carrier of V;
let Y be set ;
pred f is_bounded_on Y means :Def7: :: VFUNCT_1:def 7
ex r being Real st
for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r;
end;

:: deftheorem Def7 defines is_bounded_on VFUNCT_1:def 7 :
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for Y being set holds
( f is_bounded_on Y iff ex r being Real st
for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r );

theorem :: VFUNCT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: VFUNCT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
proof end;

theorem :: VFUNCT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st X misses dom f holds
f is_bounded_on X
proof end;

theorem :: VFUNCT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds 0 (#) f is_bounded_on Y
proof end;

theorem Th51: :: VFUNCT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
proof end;

theorem Th52: :: VFUNCT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_bounded_on Y holds
( ||.f.|| is_bounded_on Y & - f is_bounded_on Y )
proof end;

theorem Th53: :: VFUNCT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
proof end;

theorem :: VFUNCT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
proof end;

theorem :: VFUNCT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
proof end;

theorem :: VFUNCT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
proof end;

theorem :: VFUNCT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V st f1 is_constant_on X & f2 is_constant_on Y holds
( f1 + f2 is_constant_on X /\ Y & f1 - f2 is_constant_on X /\ Y )
proof end;

theorem :: VFUNCT_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C, REAL st f1 is_constant_on X & f2 is_constant_on Y holds
f1 (#) f2 is_constant_on X /\ Y
proof end;

theorem Th59: :: VFUNCT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V
for p being Real st f is_constant_on Y holds
p (#) f is_constant_on Y
proof end;

theorem Th60: :: VFUNCT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_constant_on Y holds
( ||.f.|| is_constant_on Y & - f is_constant_on Y )
proof end;

theorem Th61: :: VFUNCT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_constant_on Y holds
f is_bounded_on Y
proof end;

theorem :: VFUNCT_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_constant_on Y holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| is_bounded_on Y )
proof end;

theorem :: VFUNCT_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V st f1 is_bounded_on X & f2 is_constant_on Y holds
f1 + f2 is_bounded_on X /\ Y
proof end;

theorem :: VFUNCT_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V st f1 is_bounded_on X & f2 is_constant_on Y holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
proof end;