:: VFUNCT_1 semantic presentation

begin


definition
let C be non empty set ;
let V be non empty addLoopStr ;
let f1, f2 be PartFunc of C,V;
deffunc H1( set ) ->  Element of the U1 of V = (f1 /. $1) + (f2 /. $1);
deffunc H2( set ) ->  Element of the U1 of V = (f1 /. $1) - (f2 /. $1);
defpred S1[ set ] means $1 in (dom f1) /\ (dom f2);
set X = (dom f1) /\ (dom f2);
funcf1 + f2 ->  PartFunc of C,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,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
consider F being PartFunc of C,V such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 /. c) + (f2 /. c) ) )
thus  ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 /. c) + (f2 /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,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
thus  for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds
f /. c = H1(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
funcf1 - f2 ->  PartFunc of C,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,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
consider F being PartFunc of C,V such that
A3: for c being Element of C holds
( c in dom F iff S1[c] ) and
A4: for c being Element of C st c in dom F holds
F /. c = H2(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 /. c) - (f2 /. c) ) )
thus  ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 /. c) - (f2 /. c) ) ) by A3, A4, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,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
thus  for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds
f /. c = H2(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom g holds
g /. c = H2(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def1 defines + VFUNCT_1:def_1_:_
 for C being non empty set
for V being non empty addLoopStr
for f1, f2, b5 being PartFunc of C,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 non empty addLoopStr
for f1, f2, b5 being PartFunc of C,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) ) ) );

registration
let C be non empty set ;
let V be non empty addLoopStr ;
let f1, f2 be Function of C,V;
clusterf1 + f2 ->  total ;
coherence
 f1 + f2 is total
proof
thus  dom (f1 + f2) = (dom f1) /\ (dom f2) by Def1
.= C /\ (dom f2) by FUNCT_2:def_1
.= C /\ C by FUNCT_2:def_1
.= C ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
clusterf1 - f2 ->  total ;
coherence
 f1 - f2 is total
proof
thus  dom (f1 - f2) = (dom f1) /\ (dom f2) by Def2
.= C /\ (dom f2) by FUNCT_2:def_1
.= C /\ C by FUNCT_2:def_1
.= C ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

definition
let C be non empty set ;
let V be non empty RLSStruct ;
let f1 be PartFunc of C,REAL;
let f2 be PartFunc of C,V;
deffunc H1( Element of C) ->  Element of the U1 of V = (f1 . $1) * (f2 /. $1);
defpred S1[ set ] means $1 in (dom f1) /\ (dom f2);
set X = (dom f1) /\ (dom f2);
funcf1 (#) f2 ->  PartFunc of C,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,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
consider F being PartFunc of C,V such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 . c) * (f2 /. c) ) )
thus  ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 . c) * (f2 /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,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
thus  for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds
f /. c = H1(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def3 defines (#) VFUNCT_1:def_3_:_
 for C being non empty set
for V being non empty RLSStruct
for f1 being PartFunc of C,REAL
for f2, b5 being PartFunc of C,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) ) ) );

registration
let C be non empty set ;
let V be non empty RLSStruct ;
let f1 be Function of C,REAL;
let f2 be Function of C,V;
clusterf1 (#) f2 ->  total ;
coherence
 f1 (#) f2 is total
proof
thus  dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def3
.= C /\ (dom f2) by FUNCT_2:def_1
.= C /\ C by FUNCT_2:def_1
.= C ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

definition
let C be non empty set ;
let V be non empty RLSStruct ;
let f be PartFunc of C,V;
let r be Real;
deffunc H1( Element of C) ->  Element of the U1 of V = r * (f /. $1);
defpred S1[ set ] means $1 in dom f;
funcr (#) f ->  PartFunc of C,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,V st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = r * (f /. c) ) )
proof
consider F being PartFunc of C,V such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds
F /. c = r * (f /. c) ) )
thus  ( dom F = dom f & ( for c being Element of C st c in dom F holds
F /. c = r * (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,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
set X = dom f;
thus  for f, g being PartFunc of C,V st dom f = dom f & ( for c being Element of C st c in dom f holds
f /. c = H1(c) ) & dom g = dom f & ( for c being Element of C st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def4 defines (#) VFUNCT_1:def_4_:_
 for C being non empty set
for V being non empty RLSStruct
for f being PartFunc of C,V
for r being Real
for b5 being PartFunc of C,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) ) ) );

registration
let C be non empty set ;
let V be non empty RLSStruct ;
let f be Function of C,V;
let r be Real;
clusterr (#) f ->  total ;
coherence
 r (#) f is total
proof
thus  dom (r (#) f) = dom f by Def4
.= C by FUNCT_2:def_1 ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

definition
let C be non empty set ;
let V be non empty addLoopStr ;
let f be PartFunc of C,V;
deffunc H1( Element of C) ->  Element of the U1 of V = - (f /. $1);
defpred S1[ set ] means $1 in dom f;
func - f ->  PartFunc of C,V 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,V st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = - (f /. c) ) )
proof
consider F being PartFunc of C,V such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds
F /. c = - (f /. c) ) )
thus  ( dom F = dom f & ( for c being Element of C st c in dom F holds
F /. c = - (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,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
set X = dom f;
thus  for f, g being PartFunc of C,V st dom f = dom f & ( for c being Element of C st c in dom f holds
f /. c = H1(c) ) & dom g = dom f & ( for c being Element of C st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def5 defines - VFUNCT_1:def_5_:_
 for C being non empty set
for V being non empty addLoopStr
for f, b4 being PartFunc of C,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) ) ) );

registration
let C be non empty set ;
let V be non empty addLoopStr ;
let f be Function of C,V;
cluster - f ->  total ;
coherence
 - f is total
proof
thus  dom (- f) = dom f by Def5
.= C by FUNCT_2:def_1 ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

theorem :: VFUNCT_1:1
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,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
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,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)}))
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,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)}))
let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
let f1 be PartFunc of C,REAL; ::_thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
thus  (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) c= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) :: according to XBOOLE_0:def_10 ::_thesis: ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) or x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) )
assume A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) ; ::_thesis: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
then A2: x in dom (f1 (#) f2) by XBOOLE_0:def_5;
reconsider x1 = x as Element of C by A1;
 not x in (f1 (#) f2) " {(0. V)} by A1, XBOOLE_0:def_5;
then  not (f1 (#) f2) /. x1 in {(0. V)} by A2, PARTFUN2:26;
then  (f1 (#) f2) /. x1 <> 0. V by TARSKI:def_1;
then A3: (f1 . x1) * (f2 /. x1) <> 0. V by A2, Def3;
then  f2 /. x1 <> 0. V by RLVECT_1:10;
then  not f2 /. x1 in {(0. V)} by TARSKI:def_1;
then A4: not x1 in f2 " {(0. V)} by PARTFUN2:26;
A5: x1 in (dom f1) /\ (dom f2) by A2, Def3;
then  x1 in dom f2 by XBOOLE_0:def_4;
then A6: x in (dom f2) \ (f2 " {(0. V)}) by A4, XBOOLE_0:def_5;
 f1 . x1 <> 0 by A3, RLVECT_1:10;
then  not f1 . x1 in {0} by TARSKI:def_1;
then A7: not x1 in f1 " {0} by FUNCT_1:def_7;
 x1 in dom f1 by A5, XBOOLE_0:def_4;
then  x in (dom f1) \ (f1 " {0}) by A7, XBOOLE_0:def_5;
hence  x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) )
assume A8: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) ; ::_thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)})
then reconsider x1 = x as Element of C ;
A9: x in (dom f2) \ (f2 " {(0. V)}) by A8, XBOOLE_0:def_4;
then A10: x in dom f2 by XBOOLE_0:def_5;
 not x in f2 " {(0. V)} by A9, XBOOLE_0:def_5;
then  not f2 /. x1 in {(0. V)} by A10, PARTFUN2:26;
then A11: f2 /. x1 <> 0. V by TARSKI:def_1;
A12: x in (dom f1) \ (f1 " {0}) by A8, XBOOLE_0:def_4;
then A13: x in dom f1 by XBOOLE_0:def_5;
then  x1 in (dom f1) /\ (dom f2) by A10, XBOOLE_0:def_4;
then A14: x1 in dom (f1 (#) f2) by Def3;
 not x in f1 " {0} by A12, XBOOLE_0:def_5;
then  not f1 . x1 in {0} by A13, FUNCT_1:def_7;
then  f1 . x1 <> 0 by TARSKI:def_1;
then  (f1 . x1) * (f2 /. x1) <> 0. V by A11, RLVECT_1:11;
then  (f1 (#) f2) /. x1 <> 0. V by A14, Def3;
then  not (f1 (#) f2) /. x1 in {(0. V)} by TARSKI:def_1;
then  not x in (f1 (#) f2) " {(0. V)} by PARTFUN2:26;
hence  x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) by A14, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: VFUNCT_1:2
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let f be PartFunc of C,V; ::_thesis: ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_||.f.||_"_{0}_implies_c_in_f_"_{(0._V)}_)_&_(_c_in_f_"_{(0._V)}_implies_c_in_||.f.||_"_{0}_)_)
let c be Element of C; ::_thesis: ( ( c in ||.f.|| " {0} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in ||.f.|| " {0} ) )
thus  ( c in ||.f.|| " {0} implies c in f " {(0. V)} ) ::_thesis: ( c in f " {(0. V)} implies c in ||.f.|| " {0} )
proof
assume A1: c in ||.f.|| " {0} ; ::_thesis: c in f " {(0. V)}
then A2: c in dom ||.f.|| by FUNCT_1:def_7;
 ||.f.|| . c in {0} by A1, FUNCT_1:def_7;
then  ||.f.|| . c = 0 by TARSKI:def_1;
then  ||.(f /. c).|| = 0 by A2, NORMSP_0:def_3;
then  f /. c = 0. V by NORMSP_0:def_5;
then A3: f /. c in {(0. V)} by TARSKI:def_1;
 c in dom f by A2, NORMSP_0:def_3;
hence  c in f " {(0. V)} by A3, PARTFUN2:26; ::_thesis: verum
end;
assume A4: c in f " {(0. V)} ; ::_thesis: c in ||.f.|| " {0}
then  c in dom f by PARTFUN2:26;
then A5: c in dom ||.f.|| by NORMSP_0:def_3;
 f /. c in {(0. V)} by A4, PARTFUN2:26;
then  f /. c = 0. V by TARSKI:def_1;
then  ||.(f /. c).|| = 0 ;
then  ||.f.|| . c = 0 by A5, NORMSP_0:def_3;
then  ||.f.|| . c in {0} by TARSKI:def_1;
hence  c in ||.f.|| " {0} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
hence  ||.f.|| " {0} = f " {(0. V)} by SUBSET_1:3; ::_thesis: (- f) " {(0. V)} = f " {(0. V)}
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_(-_f)_"_{(0._V)}_implies_c_in_f_"_{(0._V)}_)_&_(_c_in_f_"_{(0._V)}_implies_c_in_(-_f)_"_{(0._V)}_)_)
let c be Element of C; ::_thesis: ( ( c in (- f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (- f) " {(0. V)} ) )
thus  ( c in (- f) " {(0. V)} implies c in f " {(0. V)} ) ::_thesis: ( c in f " {(0. V)} implies c in (- f) " {(0. V)} )
proof
assume A6: c in (- f) " {(0. V)} ; ::_thesis: c in f " {(0. V)}
then A7: c in dom (- f) by PARTFUN2:26;
 (- f) /. c in {(0. V)} by A6, PARTFUN2:26;
then  (- f) /. c = 0. V by TARSKI:def_1;
then  - (- (f /. c)) = - (0. V) by A7, Def5;
then  - (- (f /. c)) = 0. V by RLVECT_1:12;
then  f /. c = 0. V by RLVECT_1:17;
then A8: f /. c in {(0. V)} by TARSKI:def_1;
 c in dom f by A7, Def5;
hence  c in f " {(0. V)} by A8, PARTFUN2:26; ::_thesis: verum
end;
assume A9: c in f " {(0. V)} ; ::_thesis: c in (- f) " {(0. V)}
then  c in dom f by PARTFUN2:26;
then A10: c in dom (- f) by Def5;
 f /. c in {(0. V)} by A9, PARTFUN2:26;
then  f /. c = 0. V by TARSKI:def_1;
then  (- f) /. c = - (0. V) by A10, Def5;
then  (- f) /. c = 0. V by RLVECT_1:12;
then  (- f) /. c in {(0. V)} by TARSKI:def_1;
hence  c in (- f) " {(0. V)} by A10, PARTFUN2:26; ::_thesis: verum
end;
hence  (- f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; ::_thesis: verum
end;

theorem :: VFUNCT_1:3
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let f be PartFunc of C,V; ::_thesis: for r being Real st r <> 0 holds
(r (#) f) " {(0. V)} = f " {(0. V)}
let r be Real; ::_thesis: ( r <> 0 implies (r (#) f) " {(0. V)} = f " {(0. V)} )
assume A1: r <> 0 ; ::_thesis: (r (#) f) " {(0. V)} = f " {(0. V)}
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_(r_(#)_f)_"_{(0._V)}_implies_c_in_f_"_{(0._V)}_)_&_(_c_in_f_"_{(0._V)}_implies_c_in_(r_(#)_f)_"_{(0._V)}_)_)
let c be Element of C; ::_thesis: ( ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} ) )
thus  ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) ::_thesis: ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} )
proof
assume A2: c in (r (#) f) " {(0. V)} ; ::_thesis: c in f " {(0. V)}
then A3: c in dom (r (#) f) by PARTFUN2:26;
 (r (#) f) /. c in {(0. V)} by A2, PARTFUN2:26;
then  (r (#) f) /. c = 0. V by TARSKI:def_1;
then  r * (f /. c) = 0. V by A3, Def4;
then  r * (f /. c) = r * (0. V) by RLVECT_1:10;
then  f /. c = 0. V by A1, RLVECT_1:36;
then A4: f /. c in {(0. V)} by TARSKI:def_1;
 c in dom f by A3, Def4;
hence  c in f " {(0. V)} by A4, PARTFUN2:26; ::_thesis: verum
end;
assume A5: c in f " {(0. V)} ; ::_thesis: c in (r (#) f) " {(0. V)}
then  c in dom f by PARTFUN2:26;
then A6: c in dom (r (#) f) by Def4;
 f /. c in {(0. V)} by A5, PARTFUN2:26;
then  r * (f /. c) = r * (0. V) by TARSKI:def_1;
then  r * (f /. c) = 0. V by RLVECT_1:10;
then  (r (#) f) /. c = 0. V by A6, Def4;
then  (r (#) f) /. c in {(0. V)} by TARSKI:def_1;
hence  c in (r (#) f) " {(0. V)} by A6, PARTFUN2:26; ::_thesis: verum
end;
hence  (r (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; ::_thesis: verum
end;

theorem Th4: :: VFUNCT_1:4
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1
let f1, f2 be PartFunc of C,V; ::_thesis: f1 + f2 = f2 + f1
A1: dom (f1 + f2) = (dom f2) /\ (dom f1) by Def1
.= dom (f2 + f1) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_/._c_=_(f2_+_f1)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) /. c = (f2 + f1) /. c )
assume A2: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) /. c = (f2 + f1) /. c
hence (f1 + f2) /. c = (f2 /. c) + (f1 /. c) by Def1
.= (f2 + f1) /. c by A1, A2, Def1 ;
::_thesis: verum
end;
hence  f1 + f2 = f2 + f1 by A1, PARTFUN2:1; ::_thesis: verum
end;

definition
let C be non empty set ;
let V be RealNormSpace;
let f1, f2 be PartFunc of C,V;
:: original: +
redefine funcf1 + f2 ->  PartFunc of C,V;
commutativity
 for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 by Th4;
end;

theorem :: VFUNCT_1:5
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
let f1, f2, f3 be PartFunc of C,V; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3)
A1: dom ((f1 + f2) + f3) = (dom (f1 + f2)) /\ (dom f3) by Def1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by Def1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 + f3)) by Def1
.= dom (f1 + (f2 + f3)) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_+_f3)_holds_
((f1_+_f2)_+_f3)_/._c_=_(f1_+_(f2_+_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) /. c = (f1 + (f2 + f3)) /. c )
assume A2: c in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) /. c = (f1 + (f2 + f3)) /. c
then  c in (dom (f1 + f2)) /\ (dom f3) by Def1;
then A3: c in dom (f1 + f2) by XBOOLE_0:def_4;
 c in (dom f1) /\ (dom (f2 + f3)) by A1, A2, Def1;
then A4: c in dom (f2 + f3) by XBOOLE_0:def_4;
thus ((f1 + f2) + f3) /. c = ((f1 + f2) /. c) + (f3 /. c) by A2, Def1
.= ((f1 /. c) + (f2 /. c)) + (f3 /. c) by A3, Def1
.= (f1 /. c) + ((f2 /. c) + (f3 /. c)) by RLVECT_1:def_3
.= (f1 /. c) + ((f2 + f3) /. c) by A4, Def1
.= (f1 + (f2 + f3)) /. c by A1, A2, Def1 ; ::_thesis: verum
end;
hence  (f1 + f2) + f3 = f1 + (f2 + f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:6
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,REAL
for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,REAL
for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,REAL
for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let f1, f2 be PartFunc of C,REAL; ::_thesis: for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let f3 be PartFunc of C,V; ::_thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
A1: dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by Def3
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def_4
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 (#) f3)) by Def3
.= dom (f1 (#) (f2 (#) f3)) by Def3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_(#)_f3)_holds_
((f1_(#)_f2)_(#)_f3)_/._c_=_(f1_(#)_(f2_(#)_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) /. c = (f1 (#) (f2 (#) f3)) /. c )
assume A2: c in dom ((f1 (#) f2) (#) f3) ; ::_thesis: ((f1 (#) f2) (#) f3) /. c = (f1 (#) (f2 (#) f3)) /. c
then  c in (dom f1) /\ (dom (f2 (#) f3)) by A1, Def3;
then A3: c in dom (f2 (#) f3) by XBOOLE_0:def_4;
thus ((f1 (#) f2) (#) f3) /. c = ((f1 (#) f2) . c) * (f3 /. c) by A2, Def3
.= ((f1 . c) * (f2 . c)) * (f3 /. c) by VALUED_1:5
.= (f1 . c) * ((f2 . c) * (f3 /. c)) by RLVECT_1:def_7
.= (f1 . c) * ((f2 (#) f3) /. c) by A3, Def3
.= (f1 (#) (f2 (#) f3)) /. c by A1, A2, Def3 ; ::_thesis: verum
end;
hence  (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:7
for C being non empty set
for V being RealNormSpace
for f3 being PartFunc of C,V
for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f3 being PartFunc of C,V
for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let V be RealNormSpace; ::_thesis: for f3 being PartFunc of C,V
for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let f3 be PartFunc of C,V; ::_thesis: for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let f1, f2 be PartFunc of C,REAL; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by Def3
.= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:def_1
.= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16
.= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by Def3
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Def3
.= dom ((f1 (#) f3) + (f2 (#) f3)) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_(#)_f3)_holds_
((f1_+_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_+_(f2_(#)_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) (#) f3) implies ((f1 + f2) (#) f3) /. c = ((f1 (#) f3) + (f2 (#) f3)) /. c )
assume A2: c in dom ((f1 + f2) (#) f3) ; ::_thesis: ((f1 + f2) (#) f3) /. c = ((f1 (#) f3) + (f2 (#) f3)) /. c
then  c in (dom (f1 + f2)) /\ (dom f3) by Def3;
then A3: c in dom (f1 + f2) by XBOOLE_0:def_4;
A4: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, A2, Def1;
then A5: c in dom (f1 (#) f3) by XBOOLE_0:def_4;
A6: c in dom (f2 (#) f3) by A4, XBOOLE_0:def_4;
thus ((f1 + f2) (#) f3) /. c = ((f1 + f2) . c) * (f3 /. c) by A2, Def3
.= ((f1 . c) + (f2 . c)) * (f3 /. c) by A3, VALUED_1:def_1
.= ((f1 . c) * (f3 /. c)) + ((f2 . c) * (f3 /. c)) by RLVECT_1:def_6
.= ((f1 (#) f3) /. c) + ((f2 . c) * (f3 /. c)) by A5, Def3
.= ((f1 (#) f3) /. c) + ((f2 (#) f3) /. c) by A6, Def3
.= ((f1 (#) f3) + (f2 (#) f3)) /. c by A1, A2, Def1 ; ::_thesis: verum
end;
hence  (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:8
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V
for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let f1, f2 be PartFunc of C,V; ::_thesis: for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let f3 be PartFunc of C,REAL; ::_thesis: f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
A1: dom (f3 (#) (f1 + f2)) = (dom f3) /\ (dom (f1 + f2)) by Def3
.= (dom f3) /\ ((dom f1) /\ (dom f2)) by Def1
.= (((dom f3) /\ (dom f3)) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= (((dom f3) /\ (dom f1)) /\ (dom f3)) /\ (dom f2) by XBOOLE_1:16
.= ((dom f3) /\ (dom f1)) /\ ((dom f3) /\ (dom f2)) by XBOOLE_1:16
.= (dom (f3 (#) f1)) /\ ((dom f3) /\ (dom f2)) by Def3
.= (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by Def3
.= dom ((f3 (#) f1) + (f3 (#) f2)) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f3_(#)_(f1_+_f2))_holds_
(f3_(#)_(f1_+_f2))_/._c_=_((f3_(#)_f1)_+_(f3_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (f3 (#) (f1 + f2)) implies (f3 (#) (f1 + f2)) /. c = ((f3 (#) f1) + (f3 (#) f2)) /. c )
assume A2: c in dom (f3 (#) (f1 + f2)) ; ::_thesis: (f3 (#) (f1 + f2)) /. c = ((f3 (#) f1) + (f3 (#) f2)) /. c
then  c in (dom f3) /\ (dom (f1 + f2)) by Def3;
then A3: c in dom (f1 + f2) by XBOOLE_0:def_4;
A4: c in (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by A1, A2, Def1;
then A5: c in dom (f3 (#) f1) by XBOOLE_0:def_4;
A6: c in dom (f3 (#) f2) by A4, XBOOLE_0:def_4;
thus (f3 (#) (f1 + f2)) /. c = (f3 . c) * ((f1 + f2) /. c) by A2, Def3
.= (f3 . c) * ((f1 /. c) + (f2 /. c)) by A3, Def1
.= ((f3 . c) * (f1 /. c)) + ((f3 . c) * (f2 /. c)) by RLVECT_1:def_5
.= ((f3 (#) f1) /. c) + ((f3 . c) * (f2 /. c)) by A5, Def3
.= ((f3 (#) f1) /. c) + ((f3 (#) f2) /. c) by A6, Def3
.= ((f3 (#) f1) + (f3 (#) f2)) /. c by A1, A2, Def1 ; ::_thesis: verum
end;
hence  f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:9
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let f2 be PartFunc of C,V; ::_thesis: for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let r be Real; ::_thesis: for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let f1 be PartFunc of C,REAL; ::_thesis: r (#) (f1 (#) f2) = (r (#) f1) (#) f2
A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Def4
.= (dom f1) /\ (dom f2) by Def3
.= (dom (r (#) f1)) /\ (dom f2) by VALUED_1:def_5
.= dom ((r (#) f1) (#) f2) by Def3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_
(r_(#)_(f1_(#)_f2))_/._c_=_((r_(#)_f1)_(#)_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) /. c = ((r (#) f1) (#) f2) /. c )
assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) /. c = ((r (#) f1) (#) f2) /. c
then A3: c in dom (f1 (#) f2) by Def4;
 c in (dom (r (#) f1)) /\ (dom f2) by A1, A2, Def3;
then A4: c in dom (r (#) f1) by XBOOLE_0:def_4;
thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Def4
.= r * ((f1 . c) * (f2 /. c)) by A3, Def3
.= (r * (f1 . c)) * (f2 /. c) by RLVECT_1:def_7
.= ((r (#) f1) . c) * (f2 /. c) by A4, VALUED_1:def_5
.= ((r (#) f1) (#) f2) /. c by A1, A2, Def3 ; ::_thesis: verum
end;
hence  r (#) (f1 (#) f2) = (r (#) f1) (#) f2 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:10
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let f2 be PartFunc of C,V; ::_thesis: for r being Real
for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let r be Real; ::_thesis: for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let f1 be PartFunc of C,REAL; ::_thesis: r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Def4
.= (dom f1) /\ (dom f2) by Def3
.= (dom f1) /\ (dom (r (#) f2)) by Def4
.= dom (f1 (#) (r (#) f2)) by Def3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_
(r_(#)_(f1_(#)_f2))_/._c_=_(f1_(#)_(r_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) /. c = (f1 (#) (r (#) f2)) /. c )
assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) /. c = (f1 (#) (r (#) f2)) /. c
then A3: c in dom (f1 (#) f2) by Def4;
 c in (dom f1) /\ (dom (r (#) f2)) by A1, A2, Def3;
then A4: c in dom (r (#) f2) by XBOOLE_0:def_4;
thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Def4
.= r * ((f1 . c) * (f2 /. c)) by A3, Def3
.= ((f1 . c) * r) * (f2 /. c) by RLVECT_1:def_7
.= (f1 . c) * (r * (f2 /. c)) by RLVECT_1:def_7
.= (f1 . c) * ((r (#) f2) /. c) by A4, Def4
.= (f1 (#) (r (#) f2)) /. c by A1, A2, Def3 ; ::_thesis: verum
end;
hence  r (#) (f1 (#) f2) = f1 (#) (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:11
for C being non empty set
for V being RealNormSpace
for f3 being PartFunc of C,V
for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f3 being PartFunc of C,V
for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let V be RealNormSpace; ::_thesis: for f3 being PartFunc of C,V
for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let f3 be PartFunc of C,V; ::_thesis: for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let f1, f2 be PartFunc of C,REAL; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
A1: dom ((f1 - f2) (#) f3) = (dom (f1 - f2)) /\ (dom f3) by Def3
.= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:12
.= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16
.= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by Def3
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Def3
.= dom ((f1 (#) f3) - (f2 (#) f3)) by Def2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_-_f2)_(#)_f3)_holds_
((f1_-_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_-_(f2_(#)_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 - f2) (#) f3) implies ((f1 - f2) (#) f3) /. c = ((f1 (#) f3) - (f2 (#) f3)) /. c )
assume A2: c in dom ((f1 - f2) (#) f3) ; ::_thesis: ((f1 - f2) (#) f3) /. c = ((f1 (#) f3) - (f2 (#) f3)) /. c
then  c in (dom (f1 - f2)) /\ (dom f3) by Def3;
then A3: c in dom (f1 - f2) by XBOOLE_0:def_4;
A4: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, A2, Def2;
then A5: c in dom (f1 (#) f3) by XBOOLE_0:def_4;
A6: c in dom (f2 (#) f3) by A4, XBOOLE_0:def_4;
thus ((f1 - f2) (#) f3) /. c = ((f1 - f2) . c) * (f3 /. c) by A2, Def3
.= ((f1 . c) - (f2 . c)) * (f3 /. c) by A3, VALUED_1:13
.= ((f1 . c) * (f3 /. c)) - ((f2 . c) * (f3 /. c)) by RLVECT_1:35
.= ((f1 (#) f3) /. c) - ((f2 . c) * (f3 /. c)) by A5, Def3
.= ((f1 (#) f3) /. c) - ((f2 (#) f3) /. c) by A6, Def3
.= ((f1 (#) f3) - (f2 (#) f3)) /. c by A1, A2, Def2 ; ::_thesis: verum
end;
hence  (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:12
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V
for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
let f1, f2 be PartFunc of C,V; ::_thesis: for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
let f3 be PartFunc of C,REAL; ::_thesis: (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
A1: dom ((f3 (#) f1) - (f3 (#) f2)) = (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by Def2
.= (dom (f3 (#) f1)) /\ ((dom f3) /\ (dom f2)) by Def3
.= ((dom f3) /\ (dom f1)) /\ ((dom f3) /\ (dom f2)) by Def3
.= ((dom f3) /\ ((dom f3) /\ (dom f1))) /\ (dom f2) by XBOOLE_1:16
.= (((dom f3) /\ (dom f3)) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= (dom f3) /\ ((dom f1) /\ (dom f2)) by XBOOLE_1:16
.= (dom f3) /\ (dom (f1 - f2)) by Def2
.= dom (f3 (#) (f1 - f2)) by Def3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f3_(#)_(f1_-_f2))_holds_
(f3_(#)_(f1_-_f2))_/._c_=_((f3_(#)_f1)_-_(f3_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (f3 (#) (f1 - f2)) implies (f3 (#) (f1 - f2)) /. c = ((f3 (#) f1) - (f3 (#) f2)) /. c )
assume A2: c in dom (f3 (#) (f1 - f2)) ; ::_thesis: (f3 (#) (f1 - f2)) /. c = ((f3 (#) f1) - (f3 (#) f2)) /. c
then  c in (dom f3) /\ (dom (f1 - f2)) by Def3;
then A3: c in dom (f1 - f2) by XBOOLE_0:def_4;
A4: c in (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by A1, A2, Def2;
then A5: c in dom (f3 (#) f1) by XBOOLE_0:def_4;
A6: c in dom (f3 (#) f2) by A4, XBOOLE_0:def_4;
thus (f3 (#) (f1 - f2)) /. c = (f3 . c) * ((f1 - f2) /. c) by A2, Def3
.= (f3 . c) * ((f1 /. c) - (f2 /. c)) by A3, Def2
.= ((f3 . c) * (f1 /. c)) - ((f3 . c) * (f2 /. c)) by RLVECT_1:34
.= ((f3 (#) f1) /. c) - ((f3 . c) * (f2 /. c)) by A5, Def3
.= ((f3 (#) f1) /. c) - ((f3 (#) f2) /. c) by A6, Def3
.= ((f3 (#) f1) - (f3 (#) f2)) /. c by A1, A2, Def2 ; ::_thesis: verum
end;
hence  (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:13
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V
for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
let f1, f2 be PartFunc of C,V; ::_thesis: for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
let r be Real; ::_thesis: r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
A1: dom (r (#) (f1 + f2)) = dom (f1 + f2) by Def4
.= (dom f1) /\ (dom f2) by Def1
.= (dom f1) /\ (dom (r (#) f2)) by Def4
.= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Def4
.= dom ((r (#) f1) + (r (#) f2)) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_+_f2))_holds_
(r_(#)_(f1_+_f2))_/._c_=_((r_(#)_f1)_+_(r_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 + f2)) implies (r (#) (f1 + f2)) /. c = ((r (#) f1) + (r (#) f2)) /. c )
assume A2: c in dom (r (#) (f1 + f2)) ; ::_thesis: (r (#) (f1 + f2)) /. c = ((r (#) f1) + (r (#) f2)) /. c
then A3: c in dom (f1 + f2) by Def4;
A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, Def1;
then A5: c in dom (r (#) f1) by XBOOLE_0:def_4;
A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4;
thus (r (#) (f1 + f2)) /. c = r * ((f1 + f2) /. c) by A2, Def4
.= r * ((f1 /. c) + (f2 /. c)) by A3, Def1
.= (r * (f1 /. c)) + (r * (f2 /. c)) by RLVECT_1:def_5
.= ((r (#) f1) /. c) + (r * (f2 /. c)) by A5, Def4
.= ((r (#) f1) /. c) + ((r (#) f2) /. c) by A6, Def4
.= ((r (#) f1) + (r (#) f2)) /. c by A1, A2, Def1 ; ::_thesis: verum
end;
hence  r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th14: :: VFUNCT_1:14
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
let f be PartFunc of C,V; ::_thesis: for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)
let r, p be Real; ::_thesis: (r * p) (#) f = r (#) (p (#) f)
A1: dom ((r * p) (#) f) = dom f by Def4
.= dom (p (#) f) by Def4
.= dom (r (#) (p (#) f)) by Def4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_*_p)_(#)_f)_holds_
((r_*_p)_(#)_f)_/._c_=_(r_(#)_(p_(#)_f))_/._c
let c be Element of C; ::_thesis: ( c in dom ((r * p) (#) f) implies ((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c )
assume A2: c in dom ((r * p) (#) f) ; ::_thesis: ((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c
then A3: c in dom (p (#) f) by A1, Def4;
thus ((r * p) (#) f) /. c = (r * p) * (f /. c) by A2, Def4
.= r * (p * (f /. c)) by RLVECT_1:def_7
.= r * ((p (#) f) /. c) by A3, Def4
.= (r (#) (p (#) f)) /. c by A1, A2, Def4 ; ::_thesis: verum
end;
hence  (r * p) (#) f = r (#) (p (#) f) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:15
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V
for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V
for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
let f1, f2 be PartFunc of C,V; ::_thesis: for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
let r be Real; ::_thesis: r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
A1: dom (r (#) (f1 - f2)) = dom (f1 - f2) by Def4
.= (dom f1) /\ (dom f2) by Def2
.= (dom f1) /\ (dom (r (#) f2)) by Def4
.= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Def4
.= dom ((r (#) f1) - (r (#) f2)) by Def2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_-_f2))_holds_
(r_(#)_(f1_-_f2))_/._c_=_((r_(#)_f1)_-_(r_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 - f2)) implies (r (#) (f1 - f2)) /. c = ((r (#) f1) - (r (#) f2)) /. c )
assume A2: c in dom (r (#) (f1 - f2)) ; ::_thesis: (r (#) (f1 - f2)) /. c = ((r (#) f1) - (r (#) f2)) /. c
then A3: c in dom (f1 - f2) by Def4;
A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, Def2;
then A5: c in dom (r (#) f1) by XBOOLE_0:def_4;
A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4;
thus (r (#) (f1 - f2)) /. c = r * ((f1 - f2) /. c) by A2, Def4
.= r * ((f1 /. c) - (f2 /. c)) by A3, Def2
.= (r * (f1 /. c)) - (r * (f2 /. c)) by RLVECT_1:34
.= ((r (#) f1) /. c) - (r * (f2 /. c)) by A5, Def4
.= ((r (#) f1) /. c) - ((r (#) f2) /. c) by A6, Def4
.= ((r (#) f1) - (r (#) f2)) /. c by A1, A2, Def2 ; ::_thesis: verum
end;
hence  r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:16
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1)
let f1, f2 be PartFunc of C,V; ::_thesis: f1 - f2 = (- 1) (#) (f2 - f1)
A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by Def2
.= dom (f2 - f1) by Def2
.= dom ((- 1) (#) (f2 - f1)) by Def4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_/._c_=_((-_1)_(#)_(f2_-_f1))_/._c
A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by Def2
.= dom (f2 - f1) by Def2 ;
let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = ((- 1) (#) (f2 - f1)) /. c )
assume A3: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. c = ((- 1) (#) (f2 - f1)) /. c
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A3, Def2
.= - ((f2 /. c) - (f1 /. c)) by RLVECT_1:33
.= (- 1) * ((f2 /. c) - (f1 /. c)) by RLVECT_1:16
.= (- 1) * ((f2 - f1) /. c) by A3, A2, Def2
.= ((- 1) (#) (f2 - f1)) /. c by A1, A3, Def4 ; ::_thesis: verum
end;
hence  f1 - f2 = (- 1) (#) (f2 - f1) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:17
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3
let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3
let f1, f2, f3 be PartFunc of C,V; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3
A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by Def2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by Def1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by Def2
.= dom ((f1 - f2) - f3) by Def2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_+_f3))_holds_
(f1_-_(f2_+_f3))_/._c_=_((f1_-_f2)_-_f3)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) /. c = ((f1 - f2) - f3) /. c )
assume A2: c in dom (f1 - (f2 + f3)) ; ::_thesis: (f1 - (f2 + f3)) /. c = ((f1 - f2) - f3) /. c
then  c in (dom f1) /\ (dom (f2 + f3)) by Def2;
then A3: c in dom (f2 + f3) by XBOOLE_0:def_4;
 c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, Def2;
then A4: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 + f3)) /. c = (f1 /. c) - ((f2 + f3) /. c) by A2, Def2
.= (f1 /. c) - ((f2 /. c) + (f3 /. c)) by A3, Def1
.= ((f1 /. c) - (f2 /. c)) - (f3 /. c) by RLVECT_1:27
.= ((f1 - f2) /. c) - (f3 /. c) by A4, Def2
.= ((f1 - f2) - f3) /. c by A1, A2, Def2 ; ::_thesis: verum
end;
hence  f1 - (f2 + f3) = (f1 - f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th18: :: VFUNCT_1:18
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds 1 (#) f = f
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds 1 (#) f = f
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds 1 (#) f = f
let f be PartFunc of C,V; ::_thesis: 1 (#) f = f
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(1_(#)_f)_holds_
(1_(#)_f)_/._c_=_f_/._c
let c be Element of C; ::_thesis: ( c in dom (1 (#) f) implies (1 (#) f) /. c = f /. c )
assume  c in dom (1 (#) f) ; ::_thesis: (1 (#) f) /. c = f /. c
hence (1 (#) f) /. c = 1 * (f /. c) by Def4
.= f /. c by RLVECT_1:def_8 ;
::_thesis: verum
end;
 dom (1 (#) f) = dom f by Def4;
hence  1 (#) f = f by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:19
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3
let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3
let f1, f2, f3 be PartFunc of C,V; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3
A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by Def2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by Def2
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by Def2
.= dom ((f1 - f2) + f3) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_-_f3))_holds_
(f1_-_(f2_-_f3))_/._c_=_((f1_-_f2)_+_f3)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 - (f2 - f3)) implies (f1 - (f2 - f3)) /. c = ((f1 - f2) + f3) /. c )
assume A2: c in dom (f1 - (f2 - f3)) ; ::_thesis: (f1 - (f2 - f3)) /. c = ((f1 - f2) + f3) /. c
then  c in (dom f1) /\ (dom (f2 - f3)) by Def2;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
 c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, Def1;
then A4: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 - f3)) /. c = (f1 /. c) - ((f2 - f3) /. c) by A2, Def2
.= (f1 /. c) - ((f2 /. c) - (f3 /. c)) by A3, Def2
.= ((f1 /. c) - (f2 /. c)) + (f3 /. c) by RLVECT_1:29
.= ((f1 - f2) /. c) + (f3 /. c) by A4, Def2
.= ((f1 - f2) + f3) /. c by A1, A2, Def1 ; ::_thesis: verum
end;
hence  f1 - (f2 - f3) = (f1 - f2) + f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:20
for C being non empty set
for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3
let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3
let f1, f2, f3 be PartFunc of C,V; ::_thesis: f1 + (f2 - f3) = (f1 + f2) - f3
A1: dom (f1 + (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by Def1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by Def2
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 + f2)) /\ (dom f3) by Def1
.= dom ((f1 + f2) - f3) by Def2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_(f2_-_f3))_holds_
(f1_+_(f2_-_f3))_/._c_=_((f1_+_f2)_-_f3)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 + (f2 - f3)) implies (f1 + (f2 - f3)) /. c = ((f1 + f2) - f3) /. c )
assume A2: c in dom (f1 + (f2 - f3)) ; ::_thesis: (f1 + (f2 - f3)) /. c = ((f1 + f2) - f3) /. c
then  c in (dom f1) /\ (dom (f2 - f3)) by Def1;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
 c in (dom (f1 + f2)) /\ (dom f3) by A1, A2, Def2;
then A4: c in dom (f1 + f2) by XBOOLE_0:def_4;
thus (f1 + (f2 - f3)) /. c = (f1 /. c) + ((f2 - f3) /. c) by A2, Def1
.= (f1 /. c) + ((f2 /. c) - (f3 /. c)) by A3, Def2
.= ((f1 /. c) + (f2 /. c)) - (f3 /. c) by RLVECT_1:def_3
.= ((f1 + f2) /. c) - (f3 /. c) by A4, Def1
.= ((f1 + f2) - f3) /. c by A1, A2, Def2 ; ::_thesis: verum
end;
hence  f1 + (f2 - f3) = (f1 + f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:21
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
let f1 be PartFunc of C,REAL; ::_thesis: ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
A1: dom ||.(f1 (#) f2).|| = dom (f1 (#) f2) by NORMSP_0:def_3
.= (dom f1) /\ (dom f2) by Def3
.= (dom f1) /\ (dom ||.f2.||) by NORMSP_0:def_3
.= (dom (abs f1)) /\ (dom ||.f2.||) by VALUED_1:def_11
.= dom ((abs f1) (#) ||.f2.||) by VALUED_1:def_4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_||.(f1_(#)_f2).||_holds_
||.(f1_(#)_f2).||_._c_=_((abs_f1)_(#)_||.f2.||)_._c
let c be Element of C; ::_thesis: ( c in dom ||.(f1 (#) f2).|| implies ||.(f1 (#) f2).|| . c = ((abs f1) (#) ||.f2.||) . c )
assume A2: c in dom ||.(f1 (#) f2).|| ; ::_thesis: ||.(f1 (#) f2).|| . c = ((abs f1) (#) ||.f2.||) . c
then A3: c in dom (f1 (#) f2) by NORMSP_0:def_3;
 c in (dom (abs f1)) /\ (dom ||.f2.||) by A1, A2, VALUED_1:def_4;
then A4: c in dom ||.f2.|| by XBOOLE_0:def_4;
thus ||.(f1 (#) f2).|| . c = ||.((f1 (#) f2) /. c).|| by A2, NORMSP_0:def_3
.= ||.((f1 . c) * (f2 /. c)).|| by A3, Def3
.= (abs (f1 . c)) * ||.(f2 /. c).|| by NORMSP_1:def_1
.= ((abs f1) . c) * ||.(f2 /. c).|| by VALUED_1:18
.= ((abs f1) . c) * (||.f2.|| . c) by A4, NORMSP_0:def_3
.= ((abs f1) (#) ||.f2.||) . c by VALUED_1:5 ; ::_thesis: verum
end;
hence  ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem :: VFUNCT_1:22
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
let f be PartFunc of C,V; ::_thesis: for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
let r be Real; ::_thesis: ||.(r (#) f).|| = (abs r) (#) ||.f.||
A1: dom ||.(r (#) f).|| = dom (r (#) f) by NORMSP_0:def_3
.= dom f by Def4
.= dom ||.f.|| by NORMSP_0:def_3
.= dom ((abs r) (#) ||.f.||) by VALUED_1:def_5 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_||.(r_(#)_f).||_holds_
||.(r_(#)_f).||_._c_=_((abs_r)_(#)_||.f.||)_._c
let c be Element of C; ::_thesis: ( c in dom ||.(r (#) f).|| implies ||.(r (#) f).|| . c = ((abs r) (#) ||.f.||) . c )
assume A2: c in dom ||.(r (#) f).|| ; ::_thesis: ||.(r (#) f).|| . c = ((abs r) (#) ||.f.||) . c
then A3: c in dom ||.f.|| by A1, VALUED_1:def_5;
A4: c in dom (r (#) f) by A2, NORMSP_0:def_3;
thus ||.(r (#) f).|| . c = ||.((r (#) f) /. c).|| by A2, NORMSP_0:def_3
.= ||.(r * (f /. c)).|| by A4, Def4
.= (abs r) * ||.(f /. c).|| by NORMSP_1:def_1
.= (abs r) * (||.f.|| . c) by A3, NORMSP_0:def_3
.= ((abs r) (#) ||.f.||) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum
end;
hence  ||.(r (#) f).|| = (abs r) (#) ||.f.|| by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th23: :: VFUNCT_1:23
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds - f = (- 1) (#) f
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds - f = (- 1) (#) f
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds - f = (- 1) (#) f
let f be PartFunc of C,V; ::_thesis: - f = (- 1) (#) f
A1: dom (- f) = dom f by Def5
.= dom ((- 1) (#) f) by Def4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((-_1)_(#)_f)_holds_
(-_f)_/._c_=_((-_1)_(#)_f)_/._c
let c be Element of C; ::_thesis: ( c in dom ((- 1) (#) f) implies (- f) /. c = ((- 1) (#) f) /. c )
assume A2: c in dom ((- 1) (#) f) ; ::_thesis: (- f) /. c = ((- 1) (#) f) /. c
hence (- f) /. c = - (f /. c) by A1, Def5
.= (- 1) * (f /. c) by RLVECT_1:16
.= ((- 1) (#) f) /. c by A2, Def4 ;
::_thesis: verum
end;
hence  - f = (- 1) (#) f by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th24: :: VFUNCT_1:24
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds - (- f) = f
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds - (- f) = f
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds - (- f) = f
let f be PartFunc of C,V; ::_thesis: - (- f) = f
thus  - (- f) = (- 1) (#) (- f) by Th23
.= (- 1) (#) ((- 1) (#) f) by Th23
.= ((- 1) * (- 1)) (#) f by Th14
.= f by Th18 ; ::_thesis: verum
end;

theorem Th25: :: VFUNCT_1:25
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2)
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2)
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2)
let f1, f2 be PartFunc of C,V; ::_thesis: f1 - f2 = f1 + (- f2)
A1: dom (f1 - f2) = (dom f1) /\ (dom f2) by Def2
.= (dom f1) /\ (dom (- f2)) by Def5
.= dom (f1 + (- f2)) by Def1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_(-_f2))_holds_
(f1_+_(-_f2))_/._c_=_(f1_-_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 + (- f2)) implies (f1 + (- f2)) /. c = (f1 - f2) /. c )
assume A2: c in dom (f1 + (- f2)) ; ::_thesis: (f1 + (- f2)) /. c = (f1 - f2) /. c
then  c in (dom f1) /\ (dom (- f2)) by Def1;
then A3: c in dom (- f2) by XBOOLE_0:def_4;
thus (f1 + (- f2)) /. c = (f1 /. c) + ((- f2) /. c) by A2, Def1
.= (f1 /. c) - (f2 /. c) by A3, Def5
.= (f1 - f2) /. c by A1, A2, Def2 ; ::_thesis: verum
end;
hence  f1 - f2 = f1 + (- f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:26
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2
let f1, f2 be PartFunc of C,V; ::_thesis: f1 - (- f2) = f1 + f2
thus f1 - (- f2) = f1 + (- (- f2)) by Th25
.= f1 + f2 by Th24 ; ::_thesis: verum
end;

theorem Th27: :: VFUNCT_1:27
for X being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof
let X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let f1, f2 be PartFunc of C,V; ::_thesis: ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = ((f1 | X) + (f2 | X)) /. c )
assume A2: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = ((f1 | X) + (f2 | X)) /. c
then A3: c in (dom (f1 + f2)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (f1 + f2) by A3, XBOOLE_0:def_4;
then A6: c in (dom f1) /\ (dom f2) by Def1;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A4, XBOOLE_0:def_4;
then A7: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A6, XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A4, XBOOLE_0:def_4;
then A8: c in dom (f1 | X) by RELAT_1:61;
then  c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4;
then A9: c in dom ((f1 | X) + (f2 | X)) by Def1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A2, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A5, Def1
.= ((f1 | X) /. c) + (f2 /. c) by A8, PARTFUN2:15
.= ((f1 | X) /. c) + ((f2 | X) /. c) by A7, PARTFUN2:15
.= ((f1 | X) + (f2 | X)) /. c by A9, Def1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by Def1
.= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16
.= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61
.= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61
.= dom ((f1 | X) + (f2 | X)) by Def1 ;
hence  (f1 + f2) | X = (f1 | X) + (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = ((f1 | X) + f2) /. c )
assume A11: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = ((f1 | X) + f2) /. c
then A12: c in (dom (f1 + f2)) /\ X by RELAT_1:61;
then A13: c in X by XBOOLE_0:def_4;
A14: c in dom (f1 + f2) by A12, XBOOLE_0:def_4;
then A15: c in (dom f1) /\ (dom f2) by Def1;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A13, XBOOLE_0:def_4;
then A16: c in dom (f1 | X) by RELAT_1:61;
 c in dom f2 by A15, XBOOLE_0:def_4;
then  c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4;
then A17: c in dom ((f1 | X) + f2) by Def1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A11, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A14, Def1
.= ((f1 | X) /. c) + (f2 /. c) by A16, PARTFUN2:15
.= ((f1 | X) + f2) /. c by A17, Def1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by Def1
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) + f2) by Def1 ;
hence  (f1 + f2) | X = (f1 | X) + f2 by A10, PARTFUN2:1; ::_thesis: (f1 + f2) | X = f1 + (f2 | X)
A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_(f1_+_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = (f1 + (f2 | X)) /. c )
assume A19: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = (f1 + (f2 | X)) /. c
then A20: c in (dom (f1 + f2)) /\ X by RELAT_1:61;
then A21: c in X by XBOOLE_0:def_4;
A22: c in dom (f1 + f2) by A20, XBOOLE_0:def_4;
then A23: c in (dom f1) /\ (dom f2) by Def1;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A21, XBOOLE_0:def_4;
then A24: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A23, XBOOLE_0:def_4;
then  c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4;
then A25: c in dom (f1 + (f2 | X)) by Def1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A19, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A22, Def1
.= (f1 /. c) + ((f2 | X) /. c) by A24, PARTFUN2:15
.= (f1 + (f2 | X)) /. c by A25, Def1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by Def1
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 + (f2 | X)) by Def1 ;
hence  (f1 + f2) | X = f1 + (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:28
for X being set
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,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
let X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,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) )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,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) )
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,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) )
let f2 be PartFunc of C,V; ::_thesis: 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) )
let f1 be PartFunc of C,REAL; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c )
assume A2: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c
then A3: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (f1 (#) f2) by A3, XBOOLE_0:def_4;
then A6: c in (dom f1) /\ (dom f2) by Def3;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A4, XBOOLE_0:def_4;
then A7: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A6, XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A4, XBOOLE_0:def_4;
then A8: c in dom (f1 | X) by RELAT_1:61;
then  c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4;
then A9: c in dom ((f1 | X) (#) (f2 | X)) by Def3;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A2, PARTFUN2:15
.= (f1 . c) * (f2 /. c) by A5, Def3
.= ((f1 | X) . c) * (f2 /. c) by A8, FUNCT_1:47
.= ((f1 | X) . c) * ((f2 | X) /. c) by A7, PARTFUN2:15
.= ((f1 | X) (#) (f2 | X)) /. c by A9, Def3 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by Def3
.= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16
.= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61
.= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61
.= dom ((f1 | X) (#) (f2 | X)) by Def3 ;
hence  (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c )
assume A11: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c
then A12: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A13: c in X by XBOOLE_0:def_4;
A14: c in dom (f1 (#) f2) by A12, XBOOLE_0:def_4;
then A15: c in (dom f1) /\ (dom f2) by Def3;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A13, XBOOLE_0:def_4;
then A16: c in dom (f1 | X) by RELAT_1:61;
 c in dom f2 by A15, XBOOLE_0:def_4;
then  c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4;
then A17: c in dom ((f1 | X) (#) f2) by Def3;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A11, PARTFUN2:15
.= (f1 . c) * (f2 /. c) by A14, Def3
.= ((f1 | X) . c) * (f2 /. c) by A16, FUNCT_1:47
.= ((f1 | X) (#) f2) /. c by A17, Def3 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by Def3
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) (#) f2) by Def3 ;
hence  (f1 (#) f2) | X = (f1 | X) (#) f2 by A10, PARTFUN2:1; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X)
A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_(f1_(#)_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c )
assume A19: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c
then A20: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A21: c in X by XBOOLE_0:def_4;
A22: c in dom (f1 (#) f2) by A20, XBOOLE_0:def_4;
then A23: c in (dom f1) /\ (dom f2) by Def3;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A21, XBOOLE_0:def_4;
then A24: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A23, XBOOLE_0:def_4;
then  c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4;
then A25: c in dom (f1 (#) (f2 | X)) by Def3;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A19, PARTFUN2:15
.= (f1 . c) * (f2 /. c) by A22, Def3
.= (f1 . c) * ((f2 | X) /. c) by A24, PARTFUN2:15
.= (f1 (#) (f2 | X)) /. c by A25, Def3 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by Def3
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 (#) (f2 | X)) by Def3 ;
hence  (f1 (#) f2) | X = f1 (#) (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum
end;

theorem Th29: :: VFUNCT_1:29
for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
proof
let X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
let f be PartFunc of C,V; ::_thesis: ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((-_f)_|_X)_holds_
((-_f)_|_X)_/._c_=_(-_(f_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((- f) | X) implies ((- f) | X) /. c = (- (f | X)) /. c )
assume A2: c in dom ((- f) | X) ; ::_thesis: ((- f) | X) /. c = (- (f | X)) /. c
then A3: c in (dom (- f)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (- f) by A3, XBOOLE_0:def_4;
then  c in dom f by Def5;
then  c in (dom f) /\ X by A4, XBOOLE_0:def_4;
then A6: c in dom (f | X) by RELAT_1:61;
then A7: c in dom (- (f | X)) by Def5;
thus ((- f) | X) /. c = (- f) /. c by A2, PARTFUN2:15
.= - (f /. c) by A5, Def5
.= - ((f | X) /. c) by A6, PARTFUN2:15
.= (- (f | X)) /. c by A7, Def5 ; ::_thesis: verum
end;
dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61
.= (dom f) /\ X by Def5
.= dom (f | X) by RELAT_1:61
.= dom (- (f | X)) by Def5 ;
hence  (- f) | X = - (f | X) by A1, PARTFUN2:1; ::_thesis: ||.f.|| | X = ||.(f | X).||
A8: dom (||.f.|| | X) = (dom ||.f.||) /\ X by RELAT_1:61
.= (dom f) /\ X by NORMSP_0:def_3
.= dom (f | X) by RELAT_1:61
.= dom ||.(f | X).|| by NORMSP_0:def_3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(||.f.||_|_X)_holds_
(||.f.||_|_X)_._c_=_||.(f_|_X).||_._c
let c be Element of C; ::_thesis: ( c in dom (||.f.|| | X) implies (||.f.|| | X) . c = ||.(f | X).|| . c )
assume A9: c in dom (||.f.|| | X) ; ::_thesis: (||.f.|| | X) . c = ||.(f | X).|| . c
then A10: c in dom (f | X) by A8, NORMSP_0:def_3;
 c in (dom ||.f.||) /\ X by A9, RELAT_1:61;
then A11: c in dom ||.f.|| by XBOOLE_0:def_4;
thus (||.f.|| | X) . c = ||.f.|| . c by A9, FUNCT_1:47
.= ||.(f /. c).|| by A11, NORMSP_0:def_3
.= ||.((f | X) /. c).|| by A10, PARTFUN2:15
.= ||.(f | X).|| . c by A8, A9, NORMSP_0:def_3 ; ::_thesis: verum
end;
hence  ||.f.|| | X = ||.(f | X).|| by A8, PARTFUN1:5; ::_thesis: verum
end;

theorem :: VFUNCT_1:30
for X being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof
let X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let f1, f2 be PartFunc of C,V; ::_thesis: ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
thus (f1 - f2) | X = (f1 + (- f2)) | X by Th25
.= (f1 | X) + ((- f2) | X) by Th27
.= (f1 | X) + (- (f2 | X)) by Th29
.= (f1 | X) - (f2 | X) by Th25 ; ::_thesis: ( (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
thus (f1 - f2) | X = (f1 + (- f2)) | X by Th25
.= (f1 | X) + (- f2) by Th27
.= (f1 | X) - f2 by Th25 ; ::_thesis: (f1 - f2) | X = f1 - (f2 | X)
thus (f1 - f2) | X = (f1 + (- f2)) | X by Th25
.= f1 + ((- f2) | X) by Th27
.= f1 + (- (f2 | X)) by Th29
.= f1 - (f2 | X) by Th25 ; ::_thesis: verum
end;

theorem :: VFUNCT_1:31
for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds (r (#) f) | X = r (#) (f | X)
proof
let X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds (r (#) f) | X = r (#) (f | X)
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds (r (#) f) | X = r (#) (f | X)
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r being Real holds (r (#) f) | X = r (#) (f | X)
let f be PartFunc of C,V; ::_thesis: for r being Real holds (r (#) f) | X = r (#) (f | X)
let r be Real; ::_thesis: (r (#) f) | X = r (#) (f | X)
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_(#)_f)_|_X)_holds_
((r_(#)_f)_|_X)_/._c_=_(r_(#)_(f_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((r (#) f) | X) implies ((r (#) f) | X) /. c = (r (#) (f | X)) /. c )
assume A2: c in dom ((r (#) f) | X) ; ::_thesis: ((r (#) f) | X) /. c = (r (#) (f | X)) /. c
then A3: c in (dom (r (#) f)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (r (#) f) by A3, XBOOLE_0:def_4;
then  c in dom f by Def4;
then  c in (dom f) /\ X by A4, XBOOLE_0:def_4;
then A6: c in dom (f | X) by RELAT_1:61;
then A7: c in dom (r (#) (f | X)) by Def4;
thus ((r (#) f) | X) /. c = (r (#) f) /. c by A2, PARTFUN2:15
.= r * (f /. c) by A5, Def4
.= r * ((f | X) /. c) by A6, PARTFUN2:15
.= (r (#) (f | X)) /. c by A7, Def4 ; ::_thesis: verum
end;
dom ((r (#) f) | X) = (dom (r (#) f)) /\ X by RELAT_1:61
.= (dom f) /\ X by Def4
.= dom (f | X) by RELAT_1:61
.= dom (r (#) (f | X)) by Def4 ;
hence  (r (#) f) | X = r (#) (f | X) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_1:32
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,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
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,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 ) ) )
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,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 ) ) )
let f1, f2 be PartFunc of C,V; ::_thesis: ( ( 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 ) ) )
thus  ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) ::_thesis: ( ( f1 is total & f2 is total ) iff f1 - f2 is total )
proof
thus  ( f1 is total & f2 is total implies f1 + f2 is total ) ; ::_thesis: ( f1 + f2 is total implies ( f1 is total & f2 is total ) )
assume  f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 + f2) = C by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = C by Def1;
then  ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
thus  ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) ::_thesis: verum
proof
thus  ( f1 is total & f2 is total implies f1 - f2 is total ) ; ::_thesis: ( f1 - f2 is total implies ( f1 is total & f2 is total ) )
assume  f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 - f2) = C by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = C by Def2;
then  ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

theorem :: VFUNCT_1:33
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f1 be PartFunc of C,REAL; ::_thesis: ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
thus  ( f1 is total & f2 is total implies f1 (#) f2 is total ) ; ::_thesis: ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) )
assume  f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 (#) f2) = C by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = C by Def3;
then  ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th34: :: VFUNCT_1:34
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds
( f is total iff r (#) f is total )
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds
( f is total iff r (#) f is total )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r being Real holds
( f is total iff r (#) f is total )
let f be PartFunc of C,V; ::_thesis: for r being Real holds
( f is total iff r (#) f is total )
let r be Real; ::_thesis: ( f is total iff r (#) f is total )
thus  ( f is total implies r (#) f is total ) ; ::_thesis: ( r (#) f is total implies f is total )
assume  r (#) f is total ; ::_thesis: f is total
then  dom (r (#) f) = C by PARTFUN1:def_2;
hence  dom f = C by Def4; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem :: VFUNCT_1:35
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds
( f is total iff - f is total )
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds
( f is total iff - f is total )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds
( f is total iff - f is total )
let f be PartFunc of C,V; ::_thesis: ( f is total iff - f is total )
thus  ( f is total implies - f is total ) ; ::_thesis: ( - f is total implies f is total )
assume A1: - f is total ; ::_thesis: f is total
 - f = (- 1) (#) f by Th23;
hence  f is total by A1, Th34; ::_thesis: verum
end;

theorem Th36: :: VFUNCT_1:36
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds
( f is total iff ||.f.|| is total )
proof
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds
( f is total iff ||.f.|| is total )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds
( f is total iff ||.f.|| is total )
let f be PartFunc of C,V; ::_thesis: ( f is total iff ||.f.|| is total )
thus  ( f is total implies ||.f.|| is total ) ::_thesis: ( ||.f.|| is total implies f is total )
proof
assume  f is total ; ::_thesis: ||.f.|| is total
then  dom f = C by PARTFUN1:def_2;
hence  dom ||.f.|| = C by NORMSP_0:def_3; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  ||.f.|| is total ; ::_thesis: f is total
then  dom ||.f.|| = C by PARTFUN1:def_2;
hence  dom f = C by NORMSP_0:def_3; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem :: VFUNCT_1:37
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
proof
let C be non empty set ; ::_thesis: for c being Element of C
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
let c be Element of C; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is total & f2 is total implies ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
assume A1: ( f1 is total & f2 is total ) ; ::_thesis: ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
then  dom (f1 + f2) = C by PARTFUN1:def_2;
hence  (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by Def1; ::_thesis: (f1 - f2) /. c = (f1 /. c) - (f2 /. c)
 dom (f1 - f2) = C by A1, PARTFUN1:def_2;
hence  (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by Def2; ::_thesis: verum
end;

theorem :: VFUNCT_1:38
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds
(f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
proof
let C be non empty set ; ::_thesis: for c being Element of C
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds
(f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
let c be Element of C; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds
(f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds
(f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds
(f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
let f1 be PartFunc of C,REAL; ::_thesis: ( f1 is total & f2 is total implies (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) )
assume  ( f1 is total & f2 is total ) ; ::_thesis: (f1 (#) f2) /. c = (f1 . c) * (f2 /. c)
then  dom (f1 (#) f2) = C by PARTFUN1:def_2;
hence  (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) by Def3; ::_thesis: verum
end;

theorem :: VFUNCT_1:39
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
proof
let C be non empty set ; ::_thesis: for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let c be Element of C; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let f be PartFunc of C,V; ::_thesis: for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let r be Real; ::_thesis: ( f is total implies (r (#) f) /. c = r * (f /. c) )
assume  f is total ; ::_thesis: (r (#) f) /. c = r * (f /. c)
then  dom (r (#) f) = C by PARTFUN1:def_2;
hence  (r (#) f) /. c = r * (f /. c) by Def4; ::_thesis: verum
end;

theorem :: VFUNCT_1:40
for C being non empty set
for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
proof
let C be non empty set ; ::_thesis: for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let c be Element of C; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let f be PartFunc of C,V; ::_thesis: ( f is total implies ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) )
assume A1: f is total ; ::_thesis: ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
then  dom (- f) = C by PARTFUN1:def_2;
hence  (- f) /. c = - (f /. c) by Def5; ::_thesis: ||.f.|| . c = ||.(f /. c).||
 ||.f.|| is total by A1, Th36;
then  dom ||.f.|| = C by PARTFUN1:def_2;
hence  ||.f.|| . c = ||.(f /. c).|| by NORMSP_0:def_3; ::_thesis: verum
end;

definition
let C be non empty set ;
let V be non empty NORMSTR ;
let f be PartFunc of C,V;
let Y be set ;
predf is_bounded_on Y means :Def6: :: VFUNCT_1:def 6
 ex r being Real st
for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r;
end;

:: deftheorem Def6 defines is_bounded_on VFUNCT_1:def_6_:_
 for C being non empty set
for V being non empty NORMSTR
for f being PartFunc of C,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:41
for Y, X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
proof
let Y, X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
let f be PartFunc of C,V; ::_thesis: ( Y c= X & f is_bounded_on X implies f is_bounded_on Y )
assume that
A1: Y c= X and
A2: f is_bounded_on X ; ::_thesis: f is_bounded_on Y
consider r being Real such that
A3: for c being Element of C st c in X /\ (dom f) holds
||.(f /. c).|| <= r by A2, Def6;
take  r ; :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r
let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies ||.(f /. c).|| <= r )
assume  c in Y /\ (dom f) ; ::_thesis: ||.(f /. c).|| <= r
then  ( c in Y & c in dom f ) by XBOOLE_0:def_4;
then  c in X /\ (dom f) by A1, XBOOLE_0:def_4;
hence  ||.(f /. c).|| <= r by A3; ::_thesis: verum
end;

theorem :: VFUNCT_1:42
for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
proof
let X be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
let f be PartFunc of C,V; ::_thesis: ( X misses dom f implies f is_bounded_on X )
assume  X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f is_bounded_on X
then  for c being Element of C st c in X /\ (dom f) holds
||.(f /. c).|| <= 0 ;
hence  f is_bounded_on X by Def6; ::_thesis: verum
end;

theorem :: VFUNCT_1:43
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
let f be PartFunc of C,V; ::_thesis: 0 (#) f is_bounded_on Y
now__::_thesis:_ex_p_being_Element_of_NAT_st_
for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(0_(#)_f))_holds_
||.((0_(#)_f)_/._c).||_<=_p
take p = 0 ; ::_thesis: for c being Element of C st c in Y /\ (dom (0 (#) f)) holds
||.((0 (#) f) /. c).|| <= p
let c be Element of C; ::_thesis: ( c in Y /\ (dom (0 (#) f)) implies ||.((0 (#) f) /. c).|| <= p )
 0 * ||.(f /. c).|| = 0 ;
then  (abs 0) * ||.(f /. c).|| <= 0 by ABSVALUE:2;
then A1: ||.(0 * (f /. c)).|| <= 0 by NORMSP_1:def_1;
assume  c in Y /\ (dom (0 (#) f)) ; ::_thesis: ||.((0 (#) f) /. c).|| <= p
then  c in dom (0 (#) f) by XBOOLE_0:def_4;
hence  ||.((0 (#) f) /. c).|| <= p by A1, Def4; ::_thesis: verum
end;
hence  0 (#) f is_bounded_on Y by Def6; ::_thesis: verum
end;

theorem Th44: :: VFUNCT_1:44
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let f be PartFunc of C,V; ::_thesis: for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let r be Real; ::_thesis: ( f is_bounded_on Y implies r (#) f is_bounded_on Y )
assume  f is_bounded_on Y ; ::_thesis: r (#) f is_bounded_on Y
then consider r1 being Real such that
A1: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 by Def6;
take p = (abs r) * (abs r1); :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in Y /\ (dom (r (#) f)) holds
||.((r (#) f) /. c).|| <= p
let c be Element of C; ::_thesis: ( c in Y /\ (dom (r (#) f)) implies ||.((r (#) f) /. c).|| <= p )
assume A2: c in Y /\ (dom (r (#) f)) ; ::_thesis: ||.((r (#) f) /. c).|| <= p
then A3: c in Y by XBOOLE_0:def_4;
A4: c in dom (r (#) f) by A2, XBOOLE_0:def_4;
then  c in dom f by Def4;
then  c in Y /\ (dom f) by A3, XBOOLE_0:def_4;
then A5: ||.(f /. c).|| <= r1 by A1;
 r1 <= abs r1 by ABSVALUE:4;
then  ( abs r >= 0 & ||.(f /. c).|| <= abs r1 ) by A5, COMPLEX1:46, XXREAL_0:2;
then  (abs r) * ||.(f /. c).|| <= (abs r) * (abs r1) by XREAL_1:64;
then  ||.(r * (f /. c)).|| <= p by NORMSP_1:def_1;
hence  ||.((r (#) f) /. c).|| <= p by A4, Def4; ::_thesis: verum
end;

theorem Th45: :: VFUNCT_1:45
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let f be PartFunc of C,V; ::_thesis: ( f is_bounded_on Y implies ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) )
assume A1: f is_bounded_on Y ; ::_thesis: ( ||.f.|| | Y is bounded & - f is_bounded_on Y )
then consider r1 being Real such that
A2: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 by Def6;
now__::_thesis:_for_c_being_set_st_c_in_Y_/\_(dom_||.f.||)_holds_
abs_(||.f.||_._c)_<=_r1
let c be set ; ::_thesis: ( c in Y /\ (dom ||.f.||) implies abs (||.f.|| . c) <= r1 )
assume A3: c in Y /\ (dom ||.f.||) ; ::_thesis: abs (||.f.|| . c) <= r1
then A4: c in Y by XBOOLE_0:def_4;
A5: c in dom ||.f.|| by A3, XBOOLE_0:def_4;
then  c in dom f by NORMSP_0:def_3;
then  c in Y /\ (dom f) by A4, XBOOLE_0:def_4;
then  ( ||.(f /. c).|| >= 0 & ||.(f /. c).|| <= r1 ) by A2, NORMSP_1:4;
then  abs ||.(f /. c).|| <= r1 by ABSVALUE:def_1;
hence  abs (||.f.|| . c) <= r1 by A5, NORMSP_0:def_3; ::_thesis: verum
end;
hence  ||.f.|| | Y is bounded by RFUNCT_1:73; ::_thesis: - f is_bounded_on Y
 (- 1) (#) f is_bounded_on Y by A1, Th44;
hence  - f is_bounded_on Y by Th23; ::_thesis: verum
end;

theorem Th46: :: VFUNCT_1:46
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 is_bounded_on Y implies f1 + f2 is_bounded_on X /\ Y )
assume that
A1: f1 is_bounded_on X and
A2: f2 is_bounded_on Y ; ::_thesis: f1 + f2 is_bounded_on X /\ Y
consider r1 being Real such that
A3: for c being Element of C st c in X /\ (dom f1) holds
||.(f1 /. c).|| <= r1 by A1, Def6;
consider r2 being Real such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2 by A2, Def6;
take r = r1 + r2; :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
||.((f1 + f2) /. c).|| <= r
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies ||.((f1 + f2) /. c).|| <= r )
assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: ||.((f1 + f2) /. c).|| <= r
then A6: c in X /\ Y by XBOOLE_0:def_4;
then A7: c in Y by XBOOLE_0:def_4;
A8: c in dom (f1 + f2) by A5, XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom f2) by Def1;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in Y /\ (dom f2) by A7, XBOOLE_0:def_4;
then A10: ||.(f2 /. c).|| <= r2 by A4;
A11: c in X by A6, XBOOLE_0:def_4;
 c in dom f1 by A9, XBOOLE_0:def_4;
then  c in X /\ (dom f1) by A11, XBOOLE_0:def_4;
then  ||.(f1 /. c).|| <= r1 by A3;
then  ( ||.((f1 /. c) + (f2 /. c)).|| <= ||.(f1 /. c).|| + ||.(f2 /. c).|| & ||.(f1 /. c).|| + ||.(f2 /. c).|| <= r ) by A10, NORMSP_1:def_1, XREAL_1:7;
then  ||.((f1 /. c) + (f2 /. c)).|| <= r by XXREAL_0:2;
hence  ||.((f1 + f2) /. c).|| <= r by A8, Def1; ::_thesis: verum
end;

theorem :: VFUNCT_1:47
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f1 be PartFunc of C,REAL; ::_thesis: ( f1 | X is bounded & f2 is_bounded_on Y implies f1 (#) f2 is_bounded_on X /\ Y )
assume that
A1: f1 | X is bounded and
A2: f2 is_bounded_on Y ; ::_thesis: f1 (#) f2 is_bounded_on X /\ Y
consider r1 being real number  such that
A3: for c being set st c in X /\ (dom f1) holds
abs (f1 . c) <= r1 by A1, RFUNCT_1:73;
consider r2 being Real such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2 by A2, Def6;
reconsider r1 = r1 as Real by XREAL_0:def_1;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
||.((f1_(#)_f2)_/._c).||_<=_r
take r = r1 * r2; ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
||.((f1 (#) f2) /. c).|| <= r
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies ||.((f1 (#) f2) /. c).|| <= r )
assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: ||.((f1 (#) f2) /. c).|| <= r
then A6: c in X /\ Y by XBOOLE_0:def_4;
then A7: c in X by XBOOLE_0:def_4;
A8: c in dom (f1 (#) f2) by A5, XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom f2) by Def3;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in X /\ (dom f1) by A7, XBOOLE_0:def_4;
then A10: abs (f1 . c) <= r1 by A3;
A11: c in Y by A6, XBOOLE_0:def_4;
 c in dom f2 by A9, XBOOLE_0:def_4;
then  c in Y /\ (dom f2) by A11, XBOOLE_0:def_4;
then A12: ||.(f2 /. c).|| <= r2 by A4;
 ( 0 <= abs (f1 . c) & 0 <= ||.(f2 /. c).|| ) by COMPLEX1:46, NORMSP_1:4;
then  (abs (f1 . c)) * ||.(f2 /. c).|| <= r by A10, A12, XREAL_1:66;
then  ||.((f1 . c) * (f2 /. c)).|| <= r by NORMSP_1:def_1;
hence  ||.((f1 (#) f2) /. c).|| <= r by A8, Def3; ::_thesis: verum
end;
hence  f1 (#) f2 is_bounded_on X /\ Y by Def6; ::_thesis: verum
end;

theorem :: VFUNCT_1:48
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 is_bounded_on Y implies f1 - f2 is_bounded_on X /\ Y )
assume that
A1: f1 is_bounded_on X and
A2: f2 is_bounded_on Y ; ::_thesis: f1 - f2 is_bounded_on X /\ Y
 - f2 is_bounded_on Y by A2, Th45;
then  f1 + (- f2) is_bounded_on X /\ Y by A1, Th46;
hence  f1 - f2 is_bounded_on X /\ Y by Th25; ::_thesis: verum
end;

theorem :: VFUNCT_1:49
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let f be PartFunc of C,V; ::_thesis: ( f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y )
assume that
A1: f is_bounded_on X and
A2: f is_bounded_on Y ; ::_thesis: f is_bounded_on X \/ Y
consider r1 being Real such that
A3: for c being Element of C st c in X /\ (dom f) holds
||.(f /. c).|| <= r1 by A1, Def6;
consider r2 being Real such that
A4: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r2 by A2, Def6;
take r = (abs r1) + (abs r2); :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in (X \/ Y) /\ (dom f) holds
||.(f /. c).|| <= r
let c be Element of C; ::_thesis: ( c in (X \/ Y) /\ (dom f) implies ||.(f /. c).|| <= r )
assume A5: c in (X \/ Y) /\ (dom f) ; ::_thesis: ||.(f /. c).|| <= r
then A6: c in dom f by XBOOLE_0:def_4;
A7: c in X \/ Y by A5, XBOOLE_0:def_4;
now__::_thesis:_||.(f_/._c).||_<=_r
percases ( c in X or c in Y ) by A7, XBOOLE_0:def_3;
suppose c in X ; ::_thesis: ||.(f /. c).|| <= r
then  c in X /\ (dom f) by A6, XBOOLE_0:def_4;
then A8: ||.(f /. c).|| <= r1 by A3;
A9: 0 <= abs r2 by COMPLEX1:46;
 r1 <= abs r1 by ABSVALUE:4;
then  ||.(f /. c).|| <= abs r1 by A8, XXREAL_0:2;
then  ||.(f /. c).|| + 0 <= r by A9, XREAL_1:7;
hence  ||.(f /. c).|| <= r ; ::_thesis: verum
end;
suppose c in Y ; ::_thesis: ||.(f /. c).|| <= r
then  c in Y /\ (dom f) by A6, XBOOLE_0:def_4;
then A10: ||.(f /. c).|| <= r2 by A4;
A11: 0 <= abs r1 by COMPLEX1:46;
 r2 <= abs r2 by ABSVALUE:4;
then  ||.(f /. c).|| <= abs r2 by A10, XXREAL_0:2;
then  0 + ||.(f /. c).|| <= r by A11, XREAL_1:7;
hence  ||.(f /. c).|| <= r ; ::_thesis: verum
end;
end;
end;
hence  ||.(f /. c).|| <= r ; ::_thesis: verum
end;

theorem :: VFUNCT_1:50
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 | X is V8() & f2 | Y is V8() implies ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) )
assume that
A1: f1 | X is V8() and
A2: f2 | Y is V8() ; ::_thesis: ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
consider r1 being VECTOR of V such that
A3: for c being Element of C st c in X /\ (dom f1) holds
f1 /. c = r1 by A1, PARTFUN2:35;
consider r2 being VECTOR of V such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = r2 by A2, PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_
(f1_+_f2)_/._c_=_r1_+_r2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = r1 + r2 )
assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: (f1 + f2) /. c = r1 + r2
then A6: c in X /\ Y by XBOOLE_0:def_4;
then A7: c in X by XBOOLE_0:def_4;
A8: c in dom (f1 + f2) by A5, XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom f2) by Def1;
then  c in dom f1 by XBOOLE_0:def_4;
then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def_4;
A11: c in Y by A6, XBOOLE_0:def_4;
 c in dom f2 by A9, XBOOLE_0:def_4;
then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def_4;
thus (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by A8, Def1
.= r1 + (f2 /. c) by A3, A10
.= r1 + r2 by A4, A12 ; ::_thesis: verum
end;
hence  (f1 + f2) | (X /\ Y) is V8() by PARTFUN2:35; ::_thesis: (f1 - f2) | (X /\ Y) is V8()
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_-_f2))_holds_
(f1_-_f2)_/._c_=_r1_-_r2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = r1 - r2 )
assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; ::_thesis: (f1 - f2) /. c = r1 - r2
then A14: c in X /\ Y by XBOOLE_0:def_4;
then A15: c in X by XBOOLE_0:def_4;
A16: c in dom (f1 - f2) by A13, XBOOLE_0:def_4;
then A17: c in (dom f1) /\ (dom f2) by Def2;
then  c in dom f1 by XBOOLE_0:def_4;
then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def_4;
A19: c in Y by A14, XBOOLE_0:def_4;
 c in dom f2 by A17, XBOOLE_0:def_4;
then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def_4;
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A16, Def2
.= r1 - (f2 /. c) by A3, A18
.= r1 - r2 by A4, A20 ; ::_thesis: verum
end;
hence  (f1 - f2) | (X /\ Y) is V8() by PARTFUN2:35; ::_thesis: verum
end;

theorem :: VFUNCT_1:51
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let f1 be PartFunc of C,REAL; ::_thesis: ( f1 | X is V8() & f2 | Y is V8() implies (f1 (#) f2) | (X /\ Y) is V8() )
assume that
A1: f1 | X is V8() and
A2: f2 | Y is V8() ; ::_thesis: (f1 (#) f2) | (X /\ Y) is V8()
consider r1 being Real such that
A3: for c being Element of C st c in X /\ (dom f1) holds
f1 . c = r1 by A1, PARTFUN2:57;
consider r2 being VECTOR of V such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = r2 by A2, PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
(f1_(#)_f2)_/._c_=_r1_*_r2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = r1 * r2 )
assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) /. c = r1 * r2
then A6: c in X /\ Y by XBOOLE_0:def_4;
then A7: c in X by XBOOLE_0:def_4;
A8: c in dom (f1 (#) f2) by A5, XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom f2) by Def3;
then  c in dom f1 by XBOOLE_0:def_4;
then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def_4;
A11: c in Y by A6, XBOOLE_0:def_4;
 c in dom f2 by A9, XBOOLE_0:def_4;
then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def_4;
thus (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) by A8, Def3
.= r1 * (f2 /. c) by A3, A10
.= r1 * r2 by A4, A12 ; ::_thesis: verum
end;
hence  (f1 (#) f2) | (X /\ Y) is V8() by PARTFUN2:35; ::_thesis: verum
end;

theorem Th52: :: VFUNCT_1:52
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for p being Real st f | Y is V8() holds
(p (#) f) | Y is V8()
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for p being Real st f | Y is V8() holds
(p (#) f) | Y is V8()
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V
for p being Real st f | Y is V8() holds
(p (#) f) | Y is V8()
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V
for p being Real st f | Y is V8() holds
(p (#) f) | Y is V8()
let f be PartFunc of C,V; ::_thesis: for p being Real st f | Y is V8() holds
(p (#) f) | Y is V8()
let p be Real; ::_thesis: ( f | Y is V8() implies (p (#) f) | Y is V8() )
assume  f | Y is V8() ; ::_thesis: (p (#) f) | Y is V8()
then consider r being VECTOR of V such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(p_(#)_f))_holds_
(p_(#)_f)_/._c_=_p_*_r
let c be Element of C; ::_thesis: ( c in Y /\ (dom (p (#) f)) implies (p (#) f) /. c = p * r )
assume A2: c in Y /\ (dom (p (#) f)) ; ::_thesis: (p (#) f) /. c = p * r
then A3: c in Y by XBOOLE_0:def_4;
A4: c in dom (p (#) f) by A2, XBOOLE_0:def_4;
then  c in dom f by Def4;
then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4;
thus (p (#) f) /. c = p * (f /. c) by A4, Def4
.= p * r by A1, A5 ; ::_thesis: verum
end;
hence  (p (#) f) | Y is V8() by PARTFUN2:35; ::_thesis: verum
end;

theorem Th53: :: VFUNCT_1:53
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
let f be PartFunc of C,V; ::_thesis: ( f | Y is V8() implies ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) )
assume  f | Y is V8() ; ::_thesis: ( ||.f.|| | Y is V8() & (- f) | Y is V8() )
then consider r being VECTOR of V such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_||.f.||)_holds_
||.f.||_._c_=_||.r.||
let c be Element of C; ::_thesis: ( c in Y /\ (dom ||.f.||) implies ||.f.|| . c = ||.r.|| )
assume A2: c in Y /\ (dom ||.f.||) ; ::_thesis: ||.f.|| . c = ||.r.||
then A3: c in Y by XBOOLE_0:def_4;
A4: c in dom ||.f.|| by A2, XBOOLE_0:def_4;
then  c in dom f by NORMSP_0:def_3;
then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4;
thus ||.f.|| . c = ||.(f /. c).|| by A4, NORMSP_0:def_3
.= ||.r.|| by A1, A5 ; ::_thesis: verum
end;
hence  ||.f.|| | Y is V8() by PARTFUN2:57; ::_thesis: (- f) | Y is V8()
now__::_thesis:_ex_p_being_Element_of_the_U1_of_V_st_
for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(-_f))_holds_
(-_f)_/._c_=_p
take p = - r; ::_thesis: for c being Element of C st c in Y /\ (dom (- f)) holds
(- f) /. c = p
let c be Element of C; ::_thesis: ( c in Y /\ (dom (- f)) implies (- f) /. c = p )
assume A6: c in Y /\ (dom (- f)) ; ::_thesis: (- f) /. c = p
then  c in Y /\ (dom f) by Def5;
then A7: - (f /. c) = p by A1;
 c in dom (- f) by A6, XBOOLE_0:def_4;
hence  (- f) /. c = p by A7, Def5; ::_thesis: verum
end;
hence  (- f) | Y is V8() by PARTFUN2:35; ::_thesis: verum
end;

theorem Th54: :: VFUNCT_1:54
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
f is_bounded_on Y
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
f is_bounded_on Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
f is_bounded_on Y
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f | Y is V8() holds
f is_bounded_on Y
let f be PartFunc of C,V; ::_thesis: ( f | Y is V8() implies f is_bounded_on Y )
assume  f | Y is V8() ; ::_thesis: f is_bounded_on Y
then consider r being VECTOR of V such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_
||.(f_/._c).||_<=_p
take p = ||.r.||; ::_thesis: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= p
let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies ||.(f /. c).|| <= p )
assume  c in Y /\ (dom f) ; ::_thesis: ||.(f /. c).|| <= p
hence  ||.(f /. c).|| <= p by A1; ::_thesis: verum
end;
hence  f is_bounded_on Y by Def6; ::_thesis: verum
end;

theorem :: VFUNCT_1:55
for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
proof
let Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f | Y is V8() holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let f be PartFunc of C,V; ::_thesis: ( f | Y is V8() implies ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) )
assume A1: f | Y is V8() ; ::_thesis: ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
hereby  ::_thesis: ( - f is_bounded_on Y & ||.f.|| | Y is bounded )
let r be Real; ::_thesis: r (#) f is_bounded_on Y
 (r (#) f) | Y is V8() by A1, Th52;
hence  r (#) f is_bounded_on Y by Th54; ::_thesis: verum
end;
 (- f) | Y is V8() by A1, Th53;
hence  - f is_bounded_on Y by Th54; ::_thesis: ||.f.|| | Y is bounded
 ||.f.|| | Y is V8() by A1, Th53;
hence  ||.f.|| | Y is bounded ; ::_thesis: verum
end;

theorem :: VFUNCT_1:56
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
f1 + f2 is_bounded_on X /\ Y
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
f1 + f2 is_bounded_on X /\ Y
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
f1 + f2 is_bounded_on X /\ Y
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
f1 + f2 is_bounded_on X /\ Y
let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 | Y is V8() implies f1 + f2 is_bounded_on X /\ Y )
assume that
A1: f1 is_bounded_on X and
A2: f2 | Y is V8() ; ::_thesis: f1 + f2 is_bounded_on X /\ Y
 f2 is_bounded_on Y by A2, Th54;
hence  f1 + f2 is_bounded_on X /\ Y by A1, Th46; ::_thesis: verum
end;

theorem :: VFUNCT_1:57
for X, Y being set
for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
let C be non empty set ; ::_thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 | Y is V8() implies ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) )
assume that
A1: f1 is_bounded_on X and
A2: f2 | Y is V8() ; ::_thesis: ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
A3: f2 is_bounded_on Y by A2, Th54;
then  - f2 is_bounded_on Y by Th45;
then A4: f1 + (- f2) is_bounded_on X /\ Y by A1, Th46;
 - f1 is_bounded_on X by A1, Th45;
then  f2 + (- f1) is_bounded_on Y /\ X by A3, Th46;
hence  ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) by A4, Th25; ::_thesis: verum
end;