:: VFUNCT_2 semantic presentation

begin


definition
let M be non empty set ;
let V be ComplexNormSpace;
let f1 be PartFunc of M,COMPLEX;
let f2 be PartFunc of M,V;
deffunc H1( Element of M) ->  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 M,V means :Def1: :: VFUNCT_2:def 1
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom it holds
it /. c = (f1 /. c) * (f2 /. c) ) );
existence
 ex b1 being PartFunc of M,V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) * (f2 /. c) ) )
proof
consider F being PartFunc of M,V such that
A1: for c being Element of M holds
( c in dom F iff S1[c] ) and
A2: for c being Element of M 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 M st c in dom F holds
F /. c = (f1 /. c) * (f2 /. c) ) )
thus  dom F = (dom f1) /\ (dom f2) by A1, SUBSET_1:3; ::_thesis: for c being Element of M st c in dom F holds
F /. c = (f1 /. c) * (f2 /. c)
let c be Element of M; ::_thesis: ( c in dom F implies F /. c = (f1 /. c) * (f2 /. c) )
assume  c in dom F ; ::_thesis: F /. c = (f1 /. c) * (f2 /. c)
hence  F /. c = (f1 /. c) * (f2 /. c) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of M,V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) * (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b2 holds
b2 /. c = (f1 /. c) * (f2 /. c) ) holds
b1 = b2
proof
thus  for f, g being PartFunc of M,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom f holds
f /. c = H1(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def1 defines (#) VFUNCT_2:def_1_:_
 for M being non empty set
for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2, b5 being PartFunc of M,V holds
( b5 = f1 (#) f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b5 holds
b5 /. c = (f1 /. c) * (f2 /. c) ) ) );

definition
let X be non empty set ;
let V be ComplexNormSpace;
let f be PartFunc of X,V;
let z be Complex;
deffunc H1( Element of X) ->  Element of the U1 of V = z * (f /. $1);
defpred S1[ set ] means $1 in dom f;
set M = dom f;
funcz (#) f ->  PartFunc of X,V means :Def2: :: VFUNCT_2:def 2
( dom it = dom f & ( for x being Element of X st x in dom it holds
it /. x = z * (f /. x) ) );
existence
 ex b1 being PartFunc of X,V st
( dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 /. x = z * (f /. x) ) )
proof
consider F being PartFunc of X,V such that
A1: for x being Element of X holds
( x in dom F iff S1[x] ) and
A2: for x being Element of X st x in dom F holds
F /. x = H1(x) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds
F /. x = z * (f /. x) ) )
thus  dom F = dom f by A1, SUBSET_1:3; ::_thesis: for x being Element of X st x in dom F holds
F /. x = z * (f /. x)
let x be Element of X; ::_thesis: ( x in dom F implies F /. x = z * (f /. x) )
assume  x in dom F ; ::_thesis: F /. x = z * (f /. x)
hence  F /. x = z * (f /. x) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of X,V st dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 /. x = z * (f /. x) ) & dom b2 = dom f & ( for x being Element of X st x in dom b2 holds
b2 /. x = z * (f /. x) ) holds
b1 = b2
proof
thus  for f, g being PartFunc of X,V st dom f = dom f & ( for x being Element of X st x in dom f holds
f /. x = H1(x) ) & dom g = dom f & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines (#) VFUNCT_2:def_2_:_
 for X being non empty set
for V being ComplexNormSpace
for f being PartFunc of X,V
for z being Complex
for b5 being PartFunc of X,V holds
( b5 = z (#) f iff ( dom b5 = dom f & ( for x being Element of X st x in dom b5 holds
b5 /. x = z * (f /. x) ) ) );

theorem :: VFUNCT_2:1
for M being non empty set
for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
let V be ComplexNormSpace; ::_thesis: for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
let f1 be PartFunc of M,COMPLEX; ::_thesis: for f2 being PartFunc of M,V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
let f2 be PartFunc of M,V; ::_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 reconsider x1 = x as Element of M ;
A2: x in dom (f1 (#) f2) by A1, XBOOLE_0:def_5;
then A3: x1 in (dom f1) /\ (dom f2) by Def1;
 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 A4: (f1 /. x1) * (f2 /. x1) <> 0. V by A2, Def1;
then  f1 /. x1 <> 0c by CLVECT_1:1;
then A5: not f1 /. x1 in {0} by TARSKI:def_1;
 f2 /. x1 <> 0. V by A4, CLVECT_1:1;
then  not f2 /. x1 in {(0. V)} by TARSKI:def_1;
then A6: not x1 in f2 " {(0. V)} by PARTFUN2:26;
 x1 in dom f2 by A3, XBOOLE_0:def_4;
then A7: x in (dom f2) \ (f2 " {(0. V)}) by A6, XBOOLE_0:def_5;
 x1 in dom f1 by A3, XBOOLE_0:def_4;
then  not f1 . x1 in {0} by A5, PARTFUN1:def_6;
then A8: not x1 in f1 " {0} by FUNCT_1:def_7;
 x1 in dom f1 by A3, XBOOLE_0:def_4;
then  x in (dom f1) \ (f1 " {0}) by A8, XBOOLE_0:def_5;
hence  x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) by A7, 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 A9: 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 M ;
A10: x in (dom f1) \ (f1 " {0}) by A9, XBOOLE_0:def_4;
then A11: x in dom f1 by XBOOLE_0:def_5;
 not x in f1 " {0} by A10, XBOOLE_0:def_5;
then  not f1 . x1 in {0} by A11, FUNCT_1:def_7;
then  f1 . x1 <> 0 by TARSKI:def_1;
then A12: f1 /. x1 <> 0 by A11, PARTFUN1:def_6;
A13: x in (dom f2) \ (f2 " {(0. V)}) by A9, XBOOLE_0:def_4;
then A14: x in dom f2 by XBOOLE_0:def_5;
then  x1 in (dom f1) /\ (dom f2) by A11, XBOOLE_0:def_4;
then A15: x1 in dom (f1 (#) f2) by Def1;
 not x in f2 " {(0. V)} by A13, XBOOLE_0:def_5;
then  not f2 /. x1 in {(0. V)} by A14, PARTFUN2:26;
then  f2 /. x1 <> 0. V by TARSKI:def_1;
then  (f1 /. x1) * (f2 /. x1) <> 0. V by A12, CLVECT_1:2;
then  (f1 (#) f2) /. x1 <> 0. V by A15, Def1;
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 A15, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: VFUNCT_2:2
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let f be PartFunc of M,V; ::_thesis: ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
now__::_thesis:_for_c_being_Element_of_M_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 M; ::_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 by NORMSP_0:def_6;
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_M_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 M; ::_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, VFUNCT_1:def_5;
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, VFUNCT_1:def_5;
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 VFUNCT_1:def_5;
 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, VFUNCT_1:def_5;
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_2:3
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
let z be Element of COMPLEX ; ::_thesis: ( z <> 0c implies (z (#) f) " {(0. V)} = f " {(0. V)} )
assume A1: z <> 0c ; ::_thesis: (z (#) f) " {(0. V)} = f " {(0. V)}
now__::_thesis:_for_x_being_Element_of_M_holds_
(_(_x_in_(z_(#)_f)_"_{(0._V)}_implies_x_in_f_"_{(0._V)}_)_&_(_x_in_f_"_{(0._V)}_implies_x_in_(z_(#)_f)_"_{(0._V)}_)_)
let x be Element of M; ::_thesis: ( ( x in (z (#) f) " {(0. V)} implies x in f " {(0. V)} ) & ( x in f " {(0. V)} implies x in (z (#) f) " {(0. V)} ) )
thus  ( x in (z (#) f) " {(0. V)} implies x in f " {(0. V)} ) ::_thesis: ( x in f " {(0. V)} implies x in (z (#) f) " {(0. V)} )
proof
assume A2: x in (z (#) f) " {(0. V)} ; ::_thesis: x in f " {(0. V)}
then A3: x in dom (z (#) f) by PARTFUN2:26;
 (z (#) f) /. x in {(0. V)} by A2, PARTFUN2:26;
then  (z (#) f) /. x = 0. V by TARSKI:def_1;
then  z * (f /. x) = 0. V by A3, Def2;
then  z * (f /. x) = z * (0. V) by CLVECT_1:1;
then  f /. x = 0. V by A1, CLVECT_1:11;
then A4: f /. x in {(0. V)} by TARSKI:def_1;
 x in dom f by A3, Def2;
hence  x in f " {(0. V)} by A4, PARTFUN2:26; ::_thesis: verum
end;
assume A5: x in f " {(0. V)} ; ::_thesis: x in (z (#) f) " {(0. V)}
then  x in dom f by PARTFUN2:26;
then A6: x in dom (z (#) f) by Def2;
 f /. x in {(0. V)} by A5, PARTFUN2:26;
then  z * (f /. x) = z * (0. V) by TARSKI:def_1;
then  z * (f /. x) = 0. V by CLVECT_1:1;
then  (z (#) f) /. x = 0. V by A6, Def2;
then  (z (#) f) /. x in {(0. V)} by TARSKI:def_1;
hence  x in (z (#) f) " {(0. V)} by A6, PARTFUN2:26; ::_thesis: verum
end;
hence  (z (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; ::_thesis: verum
end;

theorem Th4: :: VFUNCT_2:4
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 + f2 = f2 + f1
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 + f2 = f2 + f1
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V holds f1 + f2 = f2 + f1
let f1, f2 be PartFunc of M,V; ::_thesis: f1 + f2 = f2 + f1
A1: dom (f1 + f2) = (dom f2) /\ (dom f1) by VFUNCT_1:def_1
.= dom (f2 + f1) by VFUNCT_1:def_1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_/._x_=_(f2_+_f1)_/._x
let x be Element of M; ::_thesis: ( x in dom (f1 + f2) implies (f1 + f2) /. x = (f2 + f1) /. x )
assume A2: x in dom (f1 + f2) ; ::_thesis: (f1 + f2) /. x = (f2 + f1) /. x
hence (f1 + f2) /. x = (f2 /. x) + (f1 /. x) by VFUNCT_1:def_1
.= (f2 + f1) /. x by A1, A2, VFUNCT_1:def_1 ;
::_thesis: verum
end;
hence  f1 + f2 = f2 + f1 by A1, PARTFUN2:1; ::_thesis: verum
end;

definition
let M be non empty set ;
let V be ComplexNormSpace;
let f1, f2 be PartFunc of M,V;
:: original: +
redefine funcf1 + f2 ->  Element of K6(K7(M, the U1 of V));
commutativity
 for f1, f2 being PartFunc of M,V holds f1 + f2 = f2 + f1 by Th4;
end;

theorem :: VFUNCT_2:5
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
let V be ComplexNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of M,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
let f1, f2, f3 be PartFunc of M,V; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3)
A1: dom ((f1 + f2) + f3) = (dom (f1 + f2)) /\ (dom f3) by VFUNCT_1:def_1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by VFUNCT_1:def_1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 + f3)) by VFUNCT_1:def_1
.= dom (f1 + (f2 + f3)) by VFUNCT_1:def_1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_((f1_+_f2)_+_f3)_holds_
((f1_+_f2)_+_f3)_/._x_=_(f1_+_(f2_+_f3))_/._x
let x be Element of M; ::_thesis: ( x in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) /. x = (f1 + (f2 + f3)) /. x )
assume A2: x in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) /. x = (f1 + (f2 + f3)) /. x
then  x in (dom (f1 + f2)) /\ (dom f3) by VFUNCT_1:def_1;
then A3: x in dom (f1 + f2) by XBOOLE_0:def_4;
 x in (dom f1) /\ (dom (f2 + f3)) by A1, A2, VFUNCT_1:def_1;
then A4: x in dom (f2 + f3) by XBOOLE_0:def_4;
thus ((f1 + f2) + f3) /. x = ((f1 + f2) /. x) + (f3 /. x) by A2, VFUNCT_1:def_1
.= ((f1 /. x) + (f2 /. x)) + (f3 /. x) by A3, VFUNCT_1:def_1
.= (f1 /. x) + ((f2 /. x) + (f3 /. x)) by RLVECT_1:def_3
.= (f1 /. x) + ((f2 + f3) /. x) by A4, VFUNCT_1:def_1
.= (f1 + (f2 + f3)) /. x by A1, A2, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence  (f1 + f2) + f3 = f1 + (f2 + f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:6
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,COMPLEX
for f3 being PartFunc of M,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,COMPLEX
for f3 being PartFunc of M,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,COMPLEX
for f3 being PartFunc of M,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let f1, f2 be PartFunc of M,COMPLEX; ::_thesis: for f3 being PartFunc of M,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let f3 be PartFunc of M,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 VALUED_1:def_4
.= (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_x_being_Element_of_M_st_x_in_dom_((f1_(#)_f2)_(#)_f3)_holds_
((f1_(#)_f2)_(#)_f3)_/._x_=_(f1_(#)_(f2_(#)_f3))_/._x
let x be Element of M; ::_thesis: ( x in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) /. x = (f1 (#) (f2 (#) f3)) /. x )
assume A2: x in dom ((f1 (#) f2) (#) f3) ; ::_thesis: ((f1 (#) f2) (#) f3) /. x = (f1 (#) (f2 (#) f3)) /. x
then  x in (dom (f1 (#) f2)) /\ (dom f3) by Def1;
then A3: x in dom (f1 (#) f2) by XBOOLE_0:def_4;
A4: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  x in dom f1 by A3, XBOOLE_0:def_4;
then A5: f1 . x = f1 /. x by PARTFUN1:def_6;
 x in dom f2 by A3, A4, XBOOLE_0:def_4;
then A6: f2 . x = f2 /. x by PARTFUN1:def_6;
A7: (f1 (#) f2) /. x = (f1 (#) f2) . x by A3, PARTFUN1:def_6
.= (f1 /. x) * (f2 /. x) by A3, A5, A6, VALUED_1:def_4 ;
 x in (dom f1) /\ (dom (f2 (#) f3)) by A1, A2, Def1;
then A8: x in dom (f2 (#) f3) by XBOOLE_0:def_4;
thus ((f1 (#) f2) (#) f3) /. x = ((f1 (#) f2) /. x) * (f3 /. x) by A2, Def1
.= (f1 /. x) * ((f2 /. x) * (f3 /. x)) by A7, CLVECT_1:def_4
.= (f1 /. x) * ((f2 (#) f3) /. x) by A8, Def1
.= (f1 (#) (f2 (#) f3)) /. x by A1, A2, Def1 ; ::_thesis: verum
end;
hence  (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:7
for M being non empty set
for V being ComplexNormSpace
for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let V be ComplexNormSpace; ::_thesis: for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let f3 be PartFunc of M,V; ::_thesis: for f1, f2 being PartFunc of M,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let f1, f2 be PartFunc of M,COMPLEX; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by Def1
.= ((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 Def1
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Def1
.= dom ((f1 (#) f3) + (f2 (#) f3)) by VFUNCT_1:def_1 ;
A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_((f1_+_f2)_(#)_f3)_holds_
((f1_+_f2)_(#)_f3)_/._x_=_((f1_(#)_f3)_+_(f2_(#)_f3))_/._x
let x be Element of M; ::_thesis: ( x in dom ((f1 + f2) (#) f3) implies ((f1 + f2) (#) f3) /. x = ((f1 (#) f3) + (f2 (#) f3)) /. x )
assume A3: x in dom ((f1 + f2) (#) f3) ; ::_thesis: ((f1 + f2) (#) f3) /. x = ((f1 (#) f3) + (f2 (#) f3)) /. x
then A4: x in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, VFUNCT_1:def_1;
then A5: x in dom (f1 (#) f3) by XBOOLE_0:def_4;
 x in (dom (f1 + f2)) /\ (dom f3) by A3, Def1;
then A6: x in dom (f1 + f2) by XBOOLE_0:def_4;
then  x in dom f1 by A2, XBOOLE_0:def_4;
then A7: f1 /. x = f1 . x by PARTFUN1:def_6;
 x in dom f2 by A2, A6, XBOOLE_0:def_4;
then A8: f2 /. x = f2 . x by PARTFUN1:def_6;
A9: (f1 + f2) /. x = (f1 + f2) . x by A6, PARTFUN1:def_6
.= (f1 /. x) + (f2 /. x) by A6, A7, A8, VALUED_1:def_1 ;
A10: x in dom (f2 (#) f3) by A4, XBOOLE_0:def_4;
thus ((f1 + f2) (#) f3) /. x = ((f1 + f2) /. x) * (f3 /. x) by A3, Def1
.= ((f1 /. x) * (f3 /. x)) + ((f2 /. x) * (f3 /. x)) by A9, CLVECT_1:def_3
.= ((f1 (#) f3) /. x) + ((f2 /. x) * (f3 /. x)) by A5, Def1
.= ((f1 (#) f3) /. x) + ((f2 (#) f3) /. x) by A10, Def1
.= ((f1 (#) f3) + (f2 (#) f3)) /. x by A1, A3, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence  (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:8
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let f1, f2 be PartFunc of M,V; ::_thesis: for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let f3 be PartFunc of M,COMPLEX; ::_thesis: f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
A1: dom (f3 (#) (f1 + f2)) = (dom f3) /\ (dom (f1 + f2)) by Def1
.= (dom f3) /\ ((dom f1) /\ (dom f2)) by VFUNCT_1:def_1
.= (((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 Def1
.= (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by Def1
.= dom ((f3 (#) f1) + (f3 (#) f2)) by VFUNCT_1:def_1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(f3_(#)_(f1_+_f2))_holds_
(f3_(#)_(f1_+_f2))_/._x_=_((f3_(#)_f1)_+_(f3_(#)_f2))_/._x
let x be Element of M; ::_thesis: ( x in dom (f3 (#) (f1 + f2)) implies (f3 (#) (f1 + f2)) /. x = ((f3 (#) f1) + (f3 (#) f2)) /. x )
assume A2: x in dom (f3 (#) (f1 + f2)) ; ::_thesis: (f3 (#) (f1 + f2)) /. x = ((f3 (#) f1) + (f3 (#) f2)) /. x
then  x in (dom f3) /\ (dom (f1 + f2)) by Def1;
then A3: x in dom (f1 + f2) by XBOOLE_0:def_4;
A4: x in (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by A1, A2, VFUNCT_1:def_1;
then A5: x in dom (f3 (#) f1) by XBOOLE_0:def_4;
A6: x in dom (f3 (#) f2) by A4, XBOOLE_0:def_4;
thus (f3 (#) (f1 + f2)) /. x = (f3 /. x) * ((f1 + f2) /. x) by A2, Def1
.= (f3 /. x) * ((f1 /. x) + (f2 /. x)) by A3, VFUNCT_1:def_1
.= ((f3 /. x) * (f1 /. x)) + ((f3 /. x) * (f2 /. x)) by CLVECT_1:def_2
.= ((f3 (#) f1) /. x) + ((f3 /. x) * (f2 /. x)) by A5, Def1
.= ((f3 (#) f1) /. x) + ((f3 (#) f2) /. x) by A6, Def1
.= ((f3 (#) f1) + (f3 (#) f2)) /. x by A1, A2, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence  f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:9
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let f2 be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let z be Element of COMPLEX ; ::_thesis: for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let f1 be PartFunc of M,COMPLEX; ::_thesis: z (#) (f1 (#) f2) = (z (#) f1) (#) f2
A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def1;
A2: dom (z (#) (f1 (#) f2)) = dom (f1 (#) f2) by Def2
.= (dom (z (#) f1)) /\ (dom f2) by A1, VALUED_1:def_5
.= dom ((z (#) f1) (#) f2) by Def1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(z_(#)_(f1_(#)_f2))_holds_
(z_(#)_(f1_(#)_f2))_/._x_=_((z_(#)_f1)_(#)_f2)_/._x
let x be Element of M; ::_thesis: ( x in dom (z (#) (f1 (#) f2)) implies (z (#) (f1 (#) f2)) /. x = ((z (#) f1) (#) f2) /. x )
assume A3: x in dom (z (#) (f1 (#) f2)) ; ::_thesis: (z (#) (f1 (#) f2)) /. x = ((z (#) f1) (#) f2) /. x
then  x in (dom (z (#) f1)) /\ (dom f2) by A2, Def1;
then  x in dom (z (#) f1) by XBOOLE_0:def_4;
then A4: (z (#) f1) /. x = (z (#) f1) . x by PARTFUN1:def_6;
A5: x in dom (f1 (#) f2) by A3, Def2;
then  x in dom f1 by A1, XBOOLE_0:def_4;
then A6: f1 /. x = f1 . x by PARTFUN1:def_6;
thus (z (#) (f1 (#) f2)) /. x = z * ((f1 (#) f2) /. x) by A3, Def2
.= z * ((f1 /. x) * (f2 /. x)) by A5, Def1
.= (z * (f1 /. x)) * (f2 /. x) by CLVECT_1:def_4
.= ((z (#) f1) /. x) * (f2 /. x) by A4, A6, VALUED_1:6
.= ((z (#) f1) (#) f2) /. x by A2, A3, Def1 ; ::_thesis: verum
end;
hence  z (#) (f1 (#) f2) = (z (#) f1) (#) f2 by A2, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:10
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
let f2 be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
let z be Element of COMPLEX ; ::_thesis: for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
let f1 be PartFunc of M,COMPLEX; ::_thesis: z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
A1: dom (z (#) (f1 (#) f2)) = dom (f1 (#) f2) by Def2
.= (dom f1) /\ (dom f2) by Def1
.= (dom f1) /\ (dom (z (#) f2)) by Def2
.= dom (f1 (#) (z (#) f2)) by Def1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(z_(#)_(f1_(#)_f2))_holds_
(z_(#)_(f1_(#)_f2))_/._x_=_(f1_(#)_(z_(#)_f2))_/._x
let x be Element of M; ::_thesis: ( x in dom (z (#) (f1 (#) f2)) implies (z (#) (f1 (#) f2)) /. x = (f1 (#) (z (#) f2)) /. x )
assume A2: x in dom (z (#) (f1 (#) f2)) ; ::_thesis: (z (#) (f1 (#) f2)) /. x = (f1 (#) (z (#) f2)) /. x
then A3: x in dom (f1 (#) f2) by Def2;
 x in (dom f1) /\ (dom (z (#) f2)) by A1, A2, Def1;
then A4: x in dom (z (#) f2) by XBOOLE_0:def_4;
thus (z (#) (f1 (#) f2)) /. x = z * ((f1 (#) f2) /. x) by A2, Def2
.= z * ((f1 /. x) * (f2 /. x)) by A3, Def1
.= ((f1 /. x) * z) * (f2 /. x) by CLVECT_1:def_4
.= (f1 /. x) * (z * (f2 /. x)) by CLVECT_1:def_4
.= (f1 /. x) * ((z (#) f2) /. x) by A4, Def2
.= (f1 (#) (z (#) f2)) /. x by A1, A2, Def1 ; ::_thesis: verum
end;
hence  z (#) (f1 (#) f2) = f1 (#) (z (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:11
for M being non empty set
for V being ComplexNormSpace
for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let V be ComplexNormSpace; ::_thesis: for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let f3 be PartFunc of M,V; ::_thesis: for f1, f2 being PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let f1, f2 be PartFunc of M,COMPLEX; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
A1: dom ((f1 - f2) (#) f3) = (dom (f1 + (- f2))) /\ (dom f3) by Def1
.= ((dom f1) /\ (dom (- f2))) /\ ((dom f3) /\ (dom f3)) by VALUED_1:def_1
.= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:8
.= (((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 Def1
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Def1
.= dom ((f1 (#) f3) - (f2 (#) f3)) by VFUNCT_1:def_2 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_((f1_-_f2)_(#)_f3)_holds_
((f1_-_f2)_(#)_f3)_/._x_=_((f1_(#)_f3)_-_(f2_(#)_f3))_/._x
let x be Element of M; ::_thesis: ( x in dom ((f1 - f2) (#) f3) implies ((f1 - f2) (#) f3) /. x = ((f1 (#) f3) - (f2 (#) f3)) /. x )
assume A2: x in dom ((f1 - f2) (#) f3) ; ::_thesis: ((f1 - f2) (#) f3) /. x = ((f1 (#) f3) - (f2 (#) f3)) /. x
then A3: x in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, VFUNCT_1:def_2;
then A4: x in dom (f1 (#) f3) by XBOOLE_0:def_4;
 x in (dom (f1 - f2)) /\ (dom f3) by A2, Def1;
then A5: x in dom (f1 - f2) by XBOOLE_0:def_4;
then A6: x in (dom f1) /\ (dom (- f2)) by VALUED_1:def_1;
then A7: x in dom (- f2) by XBOOLE_0:def_4;
 x in dom f1 by A6, XBOOLE_0:def_4;
then A8: f1 /. x = f1 . x by PARTFUN1:def_6;
 (f1 + (- f2)) /. x = (f1 + (- f2)) . x by A5, PARTFUN1:def_6;
then A9: (f1 + (- f2)) /. x = (f1 . x) + ((- f2) . x) by A5, VALUED_1:def_1
.= (f1 /. x) + ((- f2) /. x) by A7, A8, PARTFUN1:def_6 ;
 dom (- f2) = dom f2 by VALUED_1:8;
then A10: ( (- f2) . x = - (f2 . x) & f2 /. x = f2 . x ) by A7, PARTFUN1:def_6, VALUED_1:8;
A11: x in dom (f2 (#) f3) by A3, XBOOLE_0:def_4;
 (- f2) /. x = (- f2) . x by A7, PARTFUN1:def_6;
hence ((f1 - f2) (#) f3) /. x = ((f1 /. x) - (f2 /. x)) * (f3 /. x) by A2, A10, A9, Def1
.= ((f1 /. x) * (f3 /. x)) - ((f2 /. x) * (f3 /. x)) by CLVECT_1:10
.= ((f1 (#) f3) /. x) - ((f2 /. x) * (f3 /. x)) by A4, Def1
.= ((f1 (#) f3) /. x) - ((f2 (#) f3) /. x) by A11, Def1
.= ((f1 (#) f3) - (f2 (#) f3)) /. x by A1, A2, VFUNCT_1:def_2 ;
::_thesis: verum
end;
hence  (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:12
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
let f1, f2 be PartFunc of M,V; ::_thesis: for f3 being PartFunc of M,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
let f3 be PartFunc of M,COMPLEX; ::_thesis: (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
A1: dom ((f3 (#) f1) - (f3 (#) f2)) = (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by VFUNCT_1:def_2
.= (dom (f3 (#) f1)) /\ ((dom f3) /\ (dom f2)) by Def1
.= ((dom f3) /\ (dom f1)) /\ ((dom f3) /\ (dom f2)) by Def1
.= ((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 VFUNCT_1:def_2
.= dom (f3 (#) (f1 - f2)) by Def1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(f3_(#)_(f1_-_f2))_holds_
(f3_(#)_(f1_-_f2))_/._x_=_((f3_(#)_f1)_-_(f3_(#)_f2))_/._x
let x be Element of M; ::_thesis: ( x in dom (f3 (#) (f1 - f2)) implies (f3 (#) (f1 - f2)) /. x = ((f3 (#) f1) - (f3 (#) f2)) /. x )
assume A2: x in dom (f3 (#) (f1 - f2)) ; ::_thesis: (f3 (#) (f1 - f2)) /. x = ((f3 (#) f1) - (f3 (#) f2)) /. x
then  x in (dom f3) /\ (dom (f1 - f2)) by Def1;
then A3: x in dom (f1 - f2) by XBOOLE_0:def_4;
A4: x in (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by A1, A2, VFUNCT_1:def_2;
then A5: x in dom (f3 (#) f1) by XBOOLE_0:def_4;
A6: x in dom (f3 (#) f2) by A4, XBOOLE_0:def_4;
thus (f3 (#) (f1 - f2)) /. x = (f3 /. x) * ((f1 - f2) /. x) by A2, Def1
.= (f3 /. x) * ((f1 /. x) - (f2 /. x)) by A3, VFUNCT_1:def_2
.= ((f3 /. x) * (f1 /. x)) - ((f3 /. x) * (f2 /. x)) by CLVECT_1:9
.= ((f3 (#) f1) /. x) - ((f3 /. x) * (f2 /. x)) by A5, Def1
.= ((f3 (#) f1) /. x) - ((f3 (#) f2) /. x) by A6, Def1
.= ((f3 (#) f1) - (f3 (#) f2)) /. x by A1, A2, VFUNCT_1:def_2 ; ::_thesis: verum
end;
hence  (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:13
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)
let f1, f2 be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)
let z be Element of COMPLEX ; ::_thesis: z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)
A1: dom (z (#) (f1 + f2)) = dom (f1 + f2) by Def2
.= (dom f1) /\ (dom f2) by VFUNCT_1:def_1
.= (dom f1) /\ (dom (z (#) f2)) by Def2
.= (dom (z (#) f1)) /\ (dom (z (#) f2)) by Def2
.= dom ((z (#) f1) + (z (#) f2)) by VFUNCT_1:def_1 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(z_(#)_(f1_+_f2))_holds_
(z_(#)_(f1_+_f2))_/._x_=_((z_(#)_f1)_+_(z_(#)_f2))_/._x
let x be Element of M; ::_thesis: ( x in dom (z (#) (f1 + f2)) implies (z (#) (f1 + f2)) /. x = ((z (#) f1) + (z (#) f2)) /. x )
assume A2: x in dom (z (#) (f1 + f2)) ; ::_thesis: (z (#) (f1 + f2)) /. x = ((z (#) f1) + (z (#) f2)) /. x
then A3: x in dom (f1 + f2) by Def2;
A4: x in (dom (z (#) f1)) /\ (dom (z (#) f2)) by A1, A2, VFUNCT_1:def_1;
then A5: x in dom (z (#) f1) by XBOOLE_0:def_4;
A6: x in dom (z (#) f2) by A4, XBOOLE_0:def_4;
thus (z (#) (f1 + f2)) /. x = z * ((f1 + f2) /. x) by A2, Def2
.= z * ((f1 /. x) + (f2 /. x)) by A3, VFUNCT_1:def_1
.= (z * (f1 /. x)) + (z * (f2 /. x)) by CLVECT_1:def_2
.= ((z (#) f1) /. x) + (z * (f2 /. x)) by A5, Def2
.= ((z (#) f1) /. x) + ((z (#) f2) /. x) by A6, Def2
.= ((z (#) f1) + (z (#) f2)) /. x by A1, A2, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence  z (#) (f1 + f2) = (z (#) f1) + (z (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th14: :: VFUNCT_2:14
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z1, z2 being Element of COMPLEX holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z1, z2 being Element of COMPLEX holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z1, z2 being Element of COMPLEX holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
let f be PartFunc of M,V; ::_thesis: for z1, z2 being Element of COMPLEX holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
let z1, z2 be Element of COMPLEX ; ::_thesis: (z1 * z2) (#) f = z1 (#) (z2 (#) f)
A1: dom ((z1 * z2) (#) f) = dom f by Def2
.= dom (z2 (#) f) by Def2
.= dom (z1 (#) (z2 (#) f)) by Def2 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_((z1_*_z2)_(#)_f)_holds_
((z1_*_z2)_(#)_f)_/._x_=_(z1_(#)_(z2_(#)_f))_/._x
let x be Element of M; ::_thesis: ( x in dom ((z1 * z2) (#) f) implies ((z1 * z2) (#) f) /. x = (z1 (#) (z2 (#) f)) /. x )
assume A2: x in dom ((z1 * z2) (#) f) ; ::_thesis: ((z1 * z2) (#) f) /. x = (z1 (#) (z2 (#) f)) /. x
then A3: x in dom (z2 (#) f) by A1, Def2;
thus ((z1 * z2) (#) f) /. x = (z1 * z2) * (f /. x) by A2, Def2
.= z1 * (z2 * (f /. x)) by CLVECT_1:def_4
.= z1 * ((z2 (#) f) /. x) by A3, Def2
.= (z1 (#) (z2 (#) f)) /. x by A1, A2, Def2 ; ::_thesis: verum
end;
hence  (z1 * z2) (#) f = z1 (#) (z2 (#) f) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:15
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)
let f1, f2 be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)
let z be Element of COMPLEX ; ::_thesis: z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)
A1: dom (z (#) (f1 - f2)) = dom (f1 - f2) by Def2
.= (dom f1) /\ (dom f2) by VFUNCT_1:def_2
.= (dom f1) /\ (dom (z (#) f2)) by Def2
.= (dom (z (#) f1)) /\ (dom (z (#) f2)) by Def2
.= dom ((z (#) f1) - (z (#) f2)) by VFUNCT_1:def_2 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(z_(#)_(f1_-_f2))_holds_
(z_(#)_(f1_-_f2))_/._x_=_((z_(#)_f1)_-_(z_(#)_f2))_/._x
let x be Element of M; ::_thesis: ( x in dom (z (#) (f1 - f2)) implies (z (#) (f1 - f2)) /. x = ((z (#) f1) - (z (#) f2)) /. x )
assume A2: x in dom (z (#) (f1 - f2)) ; ::_thesis: (z (#) (f1 - f2)) /. x = ((z (#) f1) - (z (#) f2)) /. x
then A3: x in dom (f1 - f2) by Def2;
A4: x in (dom (z (#) f1)) /\ (dom (z (#) f2)) by A1, A2, VFUNCT_1:def_2;
then A5: x in dom (z (#) f1) by XBOOLE_0:def_4;
A6: x in dom (z (#) f2) by A4, XBOOLE_0:def_4;
thus (z (#) (f1 - f2)) /. x = z * ((f1 - f2) /. x) by A2, Def2
.= z * ((f1 /. x) - (f2 /. x)) by A3, VFUNCT_1:def_2
.= (z * (f1 /. x)) - (z * (f2 /. x)) by CLVECT_1:9
.= ((z (#) f1) /. x) - (z * (f2 /. x)) by A5, Def2
.= ((z (#) f1) /. x) - ((z (#) f2) /. x) by A6, Def2
.= ((z (#) f1) - (z (#) f2)) /. x by A1, A2, VFUNCT_1:def_2 ; ::_thesis: verum
end;
hence  z (#) (f1 - f2) = (z (#) f1) - (z (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:16
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - f2 = (- 1r) (#) (f2 - f1)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - f2 = (- 1r) (#) (f2 - f1)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V holds f1 - f2 = (- 1r) (#) (f2 - f1)
let f1, f2 be PartFunc of M,V; ::_thesis: f1 - f2 = (- 1r) (#) (f2 - f1)
A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by VFUNCT_1:def_2
.= dom (f2 - f1) by VFUNCT_1:def_2
.= dom ((- 1r) (#) (f2 - f1)) by Def2 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_/._x_=_((-_1r)_(#)_(f2_-_f1))_/._x
A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by VFUNCT_1:def_2
.= dom (f2 - f1) by VFUNCT_1:def_2 ;
let x be Element of M; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) /. x = ((- 1r) (#) (f2 - f1)) /. x )
assume A3: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. x = ((- 1r) (#) (f2 - f1)) /. x
thus (f1 - f2) /. x = (f1 /. x) - (f2 /. x) by A3, VFUNCT_1:def_2
.= - ((f2 /. x) - (f1 /. x)) by RLVECT_1:33
.= (- 1r) * ((f2 /. x) - (f1 /. x)) by CLVECT_1:3
.= (- 1r) * ((f2 - f1) /. x) by A3, A2, VFUNCT_1:def_2
.= ((- 1r) (#) (f2 - f1)) /. x by A1, A3, Def2 ; ::_thesis: verum
end;
hence  f1 - f2 = (- 1r) (#) (f2 - f1) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:17
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 + f3) = (f1 - f2) - f3
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 + f3) = (f1 - f2) - f3
let V be ComplexNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 + f3) = (f1 - f2) - f3
let f1, f2, f3 be PartFunc of M,V; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3
A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by VFUNCT_1:def_2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VFUNCT_1:def_1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by VFUNCT_1:def_2
.= dom ((f1 - f2) - f3) by VFUNCT_1:def_2 ;
now__::_thesis:_for_x_being_Element_of_M_st_x_in_dom_(f1_-_(f2_+_f3))_holds_
(f1_-_(f2_+_f3))_/._x_=_((f1_-_f2)_-_f3)_/._x
let x be Element of M; ::_thesis: ( x in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) /. x = ((f1 - f2) - f3) /. x )
assume A2: x in dom (f1 - (f2 + f3)) ; ::_thesis: (f1 - (f2 + f3)) /. x = ((f1 - f2) - f3) /. x
then  x in (dom f1) /\ (dom (f2 + f3)) by VFUNCT_1:def_2;
then A3: x in dom (f2 + f3) by XBOOLE_0:def_4;
 x in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VFUNCT_1:def_2;
then A4: x in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 + f3)) /. x = (f1 /. x) - ((f2 + f3) /. x) by A2, VFUNCT_1:def_2
.= (f1 /. x) - ((f2 /. x) + (f3 /. x)) by A3, VFUNCT_1:def_1
.= ((f1 /. x) - (f2 /. x)) - (f3 /. x) by RLVECT_1:27
.= ((f1 - f2) /. x) - (f3 /. x) by A4, VFUNCT_1:def_2
.= ((f1 - f2) - f3) /. x by A1, A2, VFUNCT_1:def_2 ; ::_thesis: verum
end;
hence  f1 - (f2 + f3) = (f1 - f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th18: :: VFUNCT_2:18
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds 1r (#) f = f
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds 1r (#) f = f
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V holds 1r (#) f = f
let f be PartFunc of M,V; ::_thesis: 1r (#) f = f
A1: now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_(1r_(#)_f)_holds_
(1r_(#)_f)_/._c_=_f_/._c
let c be Element of M; ::_thesis: ( c in dom (1r (#) f) implies (1r (#) f) /. c = f /. c )
assume  c in dom (1r (#) f) ; ::_thesis: (1r (#) f) /. c = f /. c
hence (1r (#) f) /. c = 1r * (f /. c) by Def2
.= f /. c by CLVECT_1:def_5 ;
::_thesis: verum
end;
 dom (1r (#) f) = dom f by Def2;
hence  1r (#) f = f by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:19
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 - f3) = (f1 - f2) + f3
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 - f3) = (f1 - f2) + f3
let V be ComplexNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 - f3) = (f1 - f2) + f3
let f1, f2, f3 be PartFunc of M,V; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3
A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VFUNCT_1:def_2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VFUNCT_1:def_2
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by VFUNCT_1:def_2
.= dom ((f1 - f2) + f3) by VFUNCT_1:def_1 ;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_(f1_-_(f2_-_f3))_holds_
(f1_-_(f2_-_f3))_/._c_=_((f1_-_f2)_+_f3)_/._c
let c be Element of M; ::_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 VFUNCT_1:def_2;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
 c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VFUNCT_1:def_1;
then A4: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 - f3)) /. c = (f1 /. c) - ((f2 - f3) /. c) by A2, VFUNCT_1:def_2
.= (f1 /. c) - ((f2 /. c) - (f3 /. c)) by A3, VFUNCT_1:def_2
.= ((f1 /. c) - (f2 /. c)) + (f3 /. c) by RLVECT_1:29
.= ((f1 - f2) /. c) + (f3 /. c) by A4, VFUNCT_1:def_2
.= ((f1 - f2) + f3) /. c by A1, A2, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence  f1 - (f2 - f3) = (f1 - f2) + f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:20
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 + (f2 - f3) = (f1 + f2) - f3
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 + (f2 - f3) = (f1 + f2) - f3
let V be ComplexNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of M,V holds f1 + (f2 - f3) = (f1 + f2) - f3
let f1, f2, f3 be PartFunc of M,V; ::_thesis: f1 + (f2 - f3) = (f1 + f2) - f3
A1: dom (f1 + (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VFUNCT_1:def_1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VFUNCT_1:def_2
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 + f2)) /\ (dom f3) by VFUNCT_1:def_1
.= dom ((f1 + f2) - f3) by VFUNCT_1:def_2 ;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_(f1_+_(f2_-_f3))_holds_
(f1_+_(f2_-_f3))_/._c_=_((f1_+_f2)_-_f3)_/._c
let c be Element of M; ::_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 VFUNCT_1:def_1;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
 c in (dom (f1 + f2)) /\ (dom f3) by A1, A2, VFUNCT_1:def_2;
then A4: c in dom (f1 + f2) by XBOOLE_0:def_4;
thus (f1 + (f2 - f3)) /. c = (f1 /. c) + ((f2 - f3) /. c) by A2, VFUNCT_1:def_1
.= (f1 /. c) + ((f2 /. c) - (f3 /. c)) by A3, VFUNCT_1:def_2
.= ((f1 /. c) + (f2 /. c)) - (f3 /. c) by RLVECT_1:def_3
.= ((f1 + f2) /. c) - (f3 /. c) by A4, VFUNCT_1:def_1
.= ((f1 + f2) - f3) /. c by A1, A2, VFUNCT_1:def_2 ; ::_thesis: verum
end;
hence  f1 + (f2 - f3) = (f1 + f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:21
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
let f2 be PartFunc of M,V; ::_thesis: for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
let f1 be PartFunc of M,COMPLEX; ::_thesis: ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def1;
A2: (dom f1) /\ (dom f2) = (dom f1) /\ (dom ||.f2.||) by NORMSP_0:def_3
.= (dom |.f1.|) /\ (dom ||.f2.||) by VALUED_1:def_11
.= dom (|.f1.| (#) ||.f2.||) by VALUED_1:def_4 ;
A3: dom ||.(f1 (#) f2).|| = dom (f1 (#) f2) by NORMSP_0:def_3;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_||.(f1_(#)_f2).||_holds_
||.(f1_(#)_f2).||_._c_=_(|.f1.|_(#)_||.f2.||)_._c
let c be Element of M; ::_thesis: ( c in dom ||.(f1 (#) f2).|| implies ||.(f1 (#) f2).|| . c = (|.f1.| (#) ||.f2.||) . c )
assume A4: c in dom ||.(f1 (#) f2).|| ; ::_thesis: ||.(f1 (#) f2).|| . c = (|.f1.| (#) ||.f2.||) . c
then  c in (dom |.f1.|) /\ (dom ||.f2.||) by A3, A1, A2, VALUED_1:def_4;
then A5: c in dom ||.f2.|| by XBOOLE_0:def_4;
A6: c in dom (f1 (#) f2) by A4, NORMSP_0:def_3;
then  c in dom f1 by A1, XBOOLE_0:def_4;
then A7: f1 /. c = f1 . c by PARTFUN1:def_6;
thus ||.(f1 (#) f2).|| . c = ||.((f1 (#) f2) /. c).|| by A4, NORMSP_0:def_3
.= ||.((f1 /. c) * (f2 /. c)).|| by A6, Def1
.= |.(f1 /. c).| * ||.(f2 /. c).|| by CLVECT_1:def_13
.= (|.f1.| . c) * ||.(f2 /. c).|| by A7, VALUED_1:18
.= (|.f1.| . c) * (||.f2.|| . c) by A5, NORMSP_0:def_3
.= (|.f1.| (#) ||.f2.||) . c by VALUED_1:5 ; ::_thesis: verum
end;
hence  ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.|| by A3, A1, A2, PARTFUN1:5; ::_thesis: verum
end;

theorem :: VFUNCT_2:22
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let z be Element of COMPLEX ; ::_thesis: ||.(z (#) f).|| = |.z.| (#) ||.f.||
A1: dom ||.(z (#) f).|| = dom (z (#) f) by NORMSP_0:def_3
.= dom f by Def2
.= dom ||.f.|| by NORMSP_0:def_3
.= dom (|.z.| (#) ||.f.||) by VALUED_1:def_5 ;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_||.(z_(#)_f).||_holds_
||.(z_(#)_f).||_._c_=_(|.z.|_(#)_||.f.||)_._c
let c be Element of M; ::_thesis: ( c in dom ||.(z (#) f).|| implies ||.(z (#) f).|| . c = (|.z.| (#) ||.f.||) . c )
assume A2: c in dom ||.(z (#) f).|| ; ::_thesis: ||.(z (#) f).|| . c = (|.z.| (#) ||.f.||) . c
then A3: c in dom ||.f.|| by A1, VALUED_1:def_5;
A4: c in dom (z (#) f) by A2, NORMSP_0:def_3;
thus ||.(z (#) f).|| . c = ||.((z (#) f) /. c).|| by A2, NORMSP_0:def_3
.= ||.(z * (f /. c)).|| by A4, Def2
.= |.z.| * ||.(f /. c).|| by CLVECT_1:def_13
.= |.z.| * (||.f.|| . c) by A3, NORMSP_0:def_3
.= (|.z.| (#) ||.f.||) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum
end;
hence  ||.(z (#) f).|| = |.z.| (#) ||.f.|| by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th23: :: VFUNCT_2:23
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds - f = (- 1r) (#) f
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds - f = (- 1r) (#) f
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V holds - f = (- 1r) (#) f
let f be PartFunc of M,V; ::_thesis: - f = (- 1r) (#) f
A1: dom (- f) = dom f by VFUNCT_1:def_5
.= dom ((- 1r) (#) f) by Def2 ;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_((-_1r)_(#)_f)_holds_
(-_f)_/._c_=_((-_1r)_(#)_f)_/._c
let c be Element of M; ::_thesis: ( c in dom ((- 1r) (#) f) implies (- f) /. c = ((- 1r) (#) f) /. c )
assume A2: c in dom ((- 1r) (#) f) ; ::_thesis: (- f) /. c = ((- 1r) (#) f) /. c
hence (- f) /. c = - (f /. c) by A1, VFUNCT_1:def_5
.= (- 1r) * (f /. c) by CLVECT_1:3
.= ((- 1r) (#) f) /. c by A2, Def2 ;
::_thesis: verum
end;
hence  - f = (- 1r) (#) f by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th24: :: VFUNCT_2:24
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds - (- f) = f
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds - (- f) = f
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V holds - (- f) = f
let f be PartFunc of M,V; ::_thesis: - (- f) = f
thus  - (- f) = (- 1r) (#) (- f) by Th23
.= (- 1r) (#) ((- 1r) (#) f) by Th23
.= ((- 1r) * (- 1r)) (#) f by Th14
.= f by Th18, COMPLEX1:def_4 ; ::_thesis: verum
end;

theorem Th25: :: VFUNCT_2:25
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - f2 = f1 + (- f2)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - f2 = f1 + (- f2)
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V holds f1 - f2 = f1 + (- f2)
let f1, f2 be PartFunc of M,V; ::_thesis: f1 - f2 = f1 + (- f2)
A1: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2
.= (dom f1) /\ (dom (- f2)) by VFUNCT_1:def_5
.= dom (f1 + (- f2)) by VFUNCT_1:def_1 ;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_(f1_+_(-_f2))_holds_
(f1_+_(-_f2))_/._c_=_(f1_-_f2)_/._c
let c be Element of M; ::_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 VFUNCT_1:def_1;
then A3: c in dom (- f2) by XBOOLE_0:def_4;
thus (f1 + (- f2)) /. c = (f1 /. c) + ((- f2) /. c) by A2, VFUNCT_1:def_1
.= (f1 /. c) - (f2 /. c) by A3, VFUNCT_1:def_5
.= (f1 - f2) /. c by A1, A2, VFUNCT_1:def_2 ; ::_thesis: verum
end;
hence  f1 - f2 = f1 + (- f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

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


theorem Th27: :: VFUNCT_2:27
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X being set holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X being set holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X being set 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 M,V; ::_thesis: for X being set holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let X be set ; ::_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_M_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_(f2_|_X))_/._c
let c be Element of M; ::_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 VFUNCT_1:def_1;
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 VFUNCT_1:def_1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A2, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A5, VFUNCT_1:def_1
.= ((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, VFUNCT_1:def_1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by VFUNCT_1:def_1
.= (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 VFUNCT_1:def_1 ;
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_M_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_f2)_/._c
let c be Element of M; ::_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 VFUNCT_1:def_1;
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 VFUNCT_1:def_1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A11, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A14, VFUNCT_1:def_1
.= ((f1 | X) /. c) + (f2 /. c) by A16, PARTFUN2:15
.= ((f1 | X) + f2) /. c by A17, VFUNCT_1:def_1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VFUNCT_1:def_1
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) + f2) by VFUNCT_1:def_1 ;
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_M_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_(f1_+_(f2_|_X))_/._c
let c be Element of M; ::_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 VFUNCT_1:def_1;
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 VFUNCT_1:def_1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A19, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A22, VFUNCT_1:def_1
.= (f1 /. c) + ((f2 | X) /. c) by A24, PARTFUN2:15
.= (f1 + (f2 | X)) /. c by A25, VFUNCT_1:def_1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VFUNCT_1:def_1
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 + (f2 | X)) by VFUNCT_1:def_1 ;
hence  (f1 + f2) | X = f1 + (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum
end;

theorem :: VFUNCT_2:28
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for X being set
for f1 being PartFunc of M,COMPLEX 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 M,V; ::_thesis: for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let X be set ; ::_thesis: for f1 being PartFunc of M,COMPLEX 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 M,COMPLEX; ::_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_M_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_(f2_|_X))_/._c
let c be Element of M; ::_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 A7: c in dom f1 by 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 A9: (f1 | X) /. c = (f1 | X) . c by PARTFUN1:def_6
.= f1 . c by A8, FUNCT_1:47
.= f1 /. c by A7, PARTFUN1:def_6 ;
 c in dom f2 by A6, XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A4, XBOOLE_0:def_4;
then A10: c in dom (f2 | X) by RELAT_1:61;
then  c in (dom (f1 | X)) /\ (dom (f2 | X)) by A8, XBOOLE_0:def_4;
then A11: 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 | X) /. c) by A10, A9, PARTFUN2:15
.= ((f1 | X) (#) (f2 | X)) /. c by A11, 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) )
A12: now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_f2)_/._c
let c be Element of M; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c )
assume A13: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c
then A14: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A15: c in dom (f1 (#) f2) by XBOOLE_0:def_4;
then A16: c in (dom f1) /\ (dom f2) by Def1;
then A17: c in dom f1 by XBOOLE_0:def_4;
 c in X by A14, XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A17, XBOOLE_0:def_4;
then A18: c in dom (f1 | X) by RELAT_1:61;
then A19: (f1 | X) /. c = (f1 | X) . c by PARTFUN1:def_6
.= f1 . c by A18, FUNCT_1:47 ;
 c in dom f2 by A16, XBOOLE_0:def_4;
then  c in (dom (f1 | X)) /\ (dom f2) by A18, XBOOLE_0:def_4;
then A20: c in dom ((f1 | X) (#) f2) by Def1;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A13, PARTFUN2:15
.= (f1 /. c) * (f2 /. c) by A15, Def1
.= ((f1 | X) /. c) * (f2 /. c) by A17, A19, PARTFUN1:def_6
.= ((f1 | X) (#) f2) /. c by A20, 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 A12, PARTFUN2:1; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X)
A21: now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_(f1_(#)_(f2_|_X))_/._c
let c be Element of M; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c )
assume A22: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c
then A23: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A24: c in X by XBOOLE_0:def_4;
A25: c in dom (f1 (#) f2) by A23, XBOOLE_0:def_4;
then A26: 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 A24, XBOOLE_0:def_4;
then A27: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A26, XBOOLE_0:def_4;
then  c in (dom f1) /\ (dom (f2 | X)) by A27, XBOOLE_0:def_4;
then A28: c in dom (f1 (#) (f2 | X)) by Def1;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A22, PARTFUN2:15
.= (f1 /. c) * (f2 /. c) by A25, Def1
.= (f1 /. c) * ((f2 | X) /. c) by A27, PARTFUN2:15
.= (f1 (#) (f2 | X)) /. c by A28, 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 A21, PARTFUN2:1; ::_thesis: verum
end;

theorem Th29: :: VFUNCT_2:29
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for X being set holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
let f be PartFunc of M,V; ::_thesis: for X being set holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
let X be set ; ::_thesis: ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )
A1: now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_((-_f)_|_X)_holds_
((-_f)_|_X)_/._c_=_(-_(f_|_X))_/._c
let c be Element of M; ::_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 VFUNCT_1:def_5;
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 VFUNCT_1:def_5;
thus ((- f) | X) /. c = (- f) /. c by A2, PARTFUN2:15
.= - (f /. c) by A5, VFUNCT_1:def_5
.= - ((f | X) /. c) by A6, PARTFUN2:15
.= (- (f | X)) /. c by A7, VFUNCT_1:def_5 ; ::_thesis: verum
end;
dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61
.= (dom f) /\ X by VFUNCT_1:def_5
.= dom (f | X) by RELAT_1:61
.= dom (- (f | X)) by VFUNCT_1:def_5 ;
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_M_st_c_in_dom_(||.f.||_|_X)_holds_
(||.f.||_|_X)_._c_=_||.(f_|_X).||_._c
let c be Element of M; ::_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_2:30
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X being set holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X being set holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X being set 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 M,V; ::_thesis: for X being set holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let X be set ; ::_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_2:31
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for X being set holds (z (#) f) | X = z (#) (f | X)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for X being set holds (z (#) f) | X = z (#) (f | X)
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX
for X being set holds (z (#) f) | X = z (#) (f | X)
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX
for X being set holds (z (#) f) | X = z (#) (f | X)
let z be Element of COMPLEX ; ::_thesis: for X being set holds (z (#) f) | X = z (#) (f | X)
let X be set ; ::_thesis: (z (#) f) | X = z (#) (f | X)
A1: now__::_thesis:_for_c_being_Element_of_M_st_c_in_dom_((z_(#)_f)_|_X)_holds_
((z_(#)_f)_|_X)_/._c_=_(z_(#)_(f_|_X))_/._c
let c be Element of M; ::_thesis: ( c in dom ((z (#) f) | X) implies ((z (#) f) | X) /. c = (z (#) (f | X)) /. c )
assume A2: c in dom ((z (#) f) | X) ; ::_thesis: ((z (#) f) | X) /. c = (z (#) (f | X)) /. c
then A3: c in (dom (z (#) f)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (z (#) f) by A3, XBOOLE_0:def_4;
then  c in dom f by Def2;
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 (z (#) (f | X)) by Def2;
thus ((z (#) f) | X) /. c = (z (#) f) /. c by A2, PARTFUN2:15
.= z * (f /. c) by A5, Def2
.= z * ((f | X) /. c) by A6, PARTFUN2:15
.= (z (#) (f | X)) /. c by A7, Def2 ; ::_thesis: verum
end;
dom ((z (#) f) | X) = (dom (z (#) f)) /\ X by RELAT_1:61
.= (dom f) /\ X by Def2
.= dom (f | X) by RELAT_1:61
.= dom (z (#) (f | X)) by Def2 ;
hence  (z (#) f) | X = z (#) (f | X) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th32: :: VFUNCT_2:32
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,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 M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,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 ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,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 M,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 ) )
proof
assume  ( f1 is total & f2 is total ) ; ::_thesis: f1 + f2 is total
then  ( dom f1 = M & dom f2 = M ) by PARTFUN1:def_2;
hence  dom (f1 + f2) = M /\ M by VFUNCT_1:def_1
.= M ;
:: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 + f2) = M by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = M by VFUNCT_1:def_1;
then  ( M c= dom f1 & M c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = M & dom f2 = M ) 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 ) )
proof
assume  ( f1 is total & f2 is total ) ; ::_thesis: f1 - f2 is total
then  ( dom f1 = M & dom f2 = M ) by PARTFUN1:def_2;
hence  dom (f1 - f2) = M /\ M by VFUNCT_1:def_2
.= M ;
:: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 - f2) = M by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = M by VFUNCT_1:def_2;
then  ( M c= dom f1 & M c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = M & dom f2 = M ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

theorem Th33: :: VFUNCT_2:33
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f2 be PartFunc of M,V; ::_thesis: for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f1 be PartFunc of M,COMPLEX; ::_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 ) )
proof
assume  ( f1 is total & f2 is total ) ; ::_thesis: f1 (#) f2 is total
then  ( dom f1 = M & dom f2 = M ) by PARTFUN1:def_2;
hence  dom (f1 (#) f2) = M /\ M by Def1
.= M ;
:: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 (#) f2) = M by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = M by Def1;
then  ( M c= dom f1 & M c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = M & dom f2 = M ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th34: :: VFUNCT_2:34
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX holds
( f is total iff z (#) f is total )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX holds
( f is total iff z (#) f is total )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX holds
( f is total iff z (#) f is total )
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX holds
( f is total iff z (#) f is total )
let z be Element of COMPLEX ; ::_thesis: ( f is total iff z (#) f is total )
thus  ( f is total implies z (#) f is total ) ::_thesis: ( z (#) f is total implies f is total )
proof
assume  f is total ; ::_thesis: z (#) f is total
then  dom f = M by PARTFUN1:def_2;
hence  dom (z (#) f) = M by Def2; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  z (#) f is total ; ::_thesis: f is total
then  dom (z (#) f) = M by PARTFUN1:def_2;
hence  dom f = M by Def2; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th35: :: VFUNCT_2:35
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff - f is total )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff - f is total )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V holds
( f is total iff - f is total )
let f be PartFunc of M,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 A1: f is total ; ::_thesis: - f is total
 - f = (- 1r) (#) f by Th23;
hence  - f is total by A1, Th34; ::_thesis: verum
end;
assume A2: - f is total ; ::_thesis: f is total
 - f = (- 1r) (#) f by Th23;
hence  f is total by A2, Th34; ::_thesis: verum
end;

theorem Th36: :: VFUNCT_2:36
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff ||.f.|| is total )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff ||.f.|| is total )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V holds
( f is total iff ||.f.|| is total )
let f be PartFunc of M,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 = M by PARTFUN1:def_2;
hence  dom ||.f.|| = M by NORMSP_0:def_3; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  ||.f.|| is total ; ::_thesis: f is total
then  dom ||.f.|| = M by PARTFUN1:def_2;
hence  dom f = M by NORMSP_0:def_3; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

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

theorem :: VFUNCT_2:38
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let f2 be PartFunc of M,V; ::_thesis: for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let f1 be PartFunc of M,COMPLEX; ::_thesis: for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let x be Element of M; ::_thesis: ( f1 is total & f2 is total implies (f1 (#) f2) /. x = (f1 /. x) * (f2 /. x) )
assume  ( f1 is total & f2 is total ) ; ::_thesis: (f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
then  f1 (#) f2 is total by Th33;
then  dom (f1 (#) f2) = M by PARTFUN1:def_2;
hence  (f1 (#) f2) /. x = (f1 /. x) * (f2 /. x) by Def1; ::_thesis: verum
end;

theorem :: VFUNCT_2:39
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let z be Element of COMPLEX ; ::_thesis: for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let x be Element of M; ::_thesis: ( f is total implies (z (#) f) /. x = z * (f /. x) )
assume  f is total ; ::_thesis: (z (#) f) /. x = z * (f /. x)
then  z (#) f is total by Th34;
then  dom (z (#) f) = M by PARTFUN1:def_2;
hence  (z (#) f) /. x = z * (f /. x) by Def2; ::_thesis: verum
end;

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

definition
let M be non empty set ;
let V be ComplexNormSpace;
let f be PartFunc of M,V;
let Y be set ;
predf is_bounded_on Y means :Def3: :: VFUNCT_2:def 3
 ex r being Real st
for x being Element of M st x in Y /\ (dom f) holds
||.(f /. x).|| <= r;
end;

:: deftheorem Def3 defines is_bounded_on VFUNCT_2:def_3_:_
 for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds
( f is_bounded_on Y iff ex r being Real st
for x being Element of M st x in Y /\ (dom f) holds
||.(f /. x).|| <= r );

theorem :: VFUNCT_2:41
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y, X being set st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y, X being set st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for Y, X being set st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
let f be PartFunc of M,V; ::_thesis: for Y, X being set st Y c= X & f is_bounded_on X holds
f is_bounded_on Y
let Y, X be set ; ::_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 x being Element of M st x in X /\ (dom f) holds
||.(f /. x).|| <= r by A2, Def3;
take  r ; :: according to VFUNCT_2:def_3 ::_thesis: for x being Element of M st x in Y /\ (dom f) holds
||.(f /. x).|| <= r
let x be Element of M; ::_thesis: ( x in Y /\ (dom f) implies ||.(f /. x).|| <= r )
assume  x in Y /\ (dom f) ; ::_thesis: ||.(f /. x).|| <= r
then  ( x in Y & x in dom f ) by XBOOLE_0:def_4;
then  x in X /\ (dom f) by A1, XBOOLE_0:def_4;
hence  ||.(f /. x).|| <= r by A3; ::_thesis: verum
end;

theorem :: VFUNCT_2:42
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set st X misses dom f holds
f is_bounded_on X
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set st X misses dom f holds
f is_bounded_on X
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for X being set st X misses dom f holds
f is_bounded_on X
let f be PartFunc of M,V; ::_thesis: for X being set st X misses dom f holds
f is_bounded_on X
let X be set ; ::_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 x being Element of M st x in X /\ (dom f) holds
||.(f /. x).|| <= 0 ;
hence  f is_bounded_on X by Def3; ::_thesis: verum
end;

theorem :: VFUNCT_2:43
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds 0c (#) f is_bounded_on Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds 0c (#) f is_bounded_on Y
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for Y being set holds 0c (#) f is_bounded_on Y
let f be PartFunc of M,V; ::_thesis: for Y being set holds 0c (#) f is_bounded_on Y
let Y be set ; ::_thesis: 0c (#) f is_bounded_on Y
now__::_thesis:_ex_p_being_Element_of_NAT_st_
for_c_being_Element_of_M_st_c_in_Y_/\_(dom_(0c_(#)_f))_holds_
||.((0c_(#)_f)_/._c).||_<=_p
take p = 0 ; ::_thesis: for c being Element of M st c in Y /\ (dom (0c (#) f)) holds
||.((0c (#) f) /. c).|| <= p
let c be Element of M; ::_thesis: ( c in Y /\ (dom (0c (#) f)) implies ||.((0c (#) f) /. c).|| <= p )
 |.0c.| * ||.(f /. c).|| <= 0 by COMPLEX1:44;
then A1: ||.(0c * (f /. c)).|| <= 0 by CLVECT_1:def_13;
assume  c in Y /\ (dom (0c (#) f)) ; ::_thesis: ||.((0c (#) f) /. c).|| <= p
then  c in dom (0c (#) f) by XBOOLE_0:def_4;
hence  ||.((0c (#) f) /. c).|| <= p by A1, Def2; ::_thesis: verum
end;
hence  0c (#) f is_bounded_on Y by Def3; ::_thesis: verum
end;

theorem Th44: :: VFUNCT_2:44
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let z be Element of COMPLEX ; ::_thesis: for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let Y be set ; ::_thesis: ( f is_bounded_on Y implies z (#) f is_bounded_on Y )
assume  f is_bounded_on Y ; ::_thesis: z (#) f is_bounded_on Y
then consider r1 being Real such that
A1: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 by Def3;
take p = |.z.| * (abs r1); :: according to VFUNCT_2:def_3 ::_thesis: for x being Element of M st x in Y /\ (dom (z (#) f)) holds
||.((z (#) f) /. x).|| <= p
let c be Element of M; ::_thesis: ( c in Y /\ (dom (z (#) f)) implies ||.((z (#) f) /. c).|| <= p )
assume A2: c in Y /\ (dom (z (#) f)) ; ::_thesis: ||.((z (#) f) /. c).|| <= p
then A3: c in Y by XBOOLE_0:def_4;
A4: c in dom (z (#) f) by A2, XBOOLE_0:def_4;
then  c in dom f by Def2;
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  ( |.z.| >= 0 & ||.(f /. c).|| <= abs r1 ) by A5, COMPLEX1:46, XXREAL_0:2;
then  |.z.| * ||.(f /. c).|| <= |.z.| * (abs r1) by XREAL_1:64;
then  ||.(z * (f /. c)).|| <= p by CLVECT_1:def_13;
hence  ||.((z (#) f) /. c).|| <= p by A4, Def2; ::_thesis: verum
end;

theorem Th45: :: VFUNCT_2:45
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let f be PartFunc of M,V; ::_thesis: for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let Y be set ; ::_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 M st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 by Def3;
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, CLVECT_1:105;
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
 (- 1r) (#) f is_bounded_on Y by A1, Th44;
hence  - f is_bounded_on Y by Th23; ::_thesis: verum
end;

theorem Th46: :: VFUNCT_2:46
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X, Y being set 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 M,V; ::_thesis: for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let X, Y be set ; ::_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 M st c in X /\ (dom f1) holds
||.(f1 /. c).|| <= r1 by A1, Def3;
consider r2 being Real such that
A4: for c being Element of M st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2 by A2, Def3;
take r = r1 + r2; :: according to VFUNCT_2:def_3 ::_thesis: for x being Element of M st x in (X /\ Y) /\ (dom (f1 + f2)) holds
||.((f1 + f2) /. x).|| <= r
let c be Element of M; ::_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 VFUNCT_1:def_1;
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, CLVECT_1:def_13, XREAL_1:7;
then  ||.((f1 /. c) + (f2 /. c)).|| <= r by XXREAL_0:2;
hence  ||.((f1 + f2) /. c).|| <= r by A8, VFUNCT_1:def_1; ::_thesis: verum
end;

theorem :: VFUNCT_2:47
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f2 be PartFunc of M,V; ::_thesis: for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let X, Y be set ; ::_thesis: for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f1 be PartFunc of M,COMPLEX; ::_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 Element of M st c in X /\ (dom f1) holds
|.(f1 /. c).| <= r1 by A1, CFUNCT_1:69;
consider r2 being Real such that
A4: for c being Element of M st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2 by A2, Def3;
reconsider r1 = r1 as Real by XREAL_0:def_1;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
for_c_being_Element_of_M_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
||.((f1_(#)_f2)_/._c).||_<=_r
take r = r1 * r2; ::_thesis: for c being Element of M st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
||.((f1 (#) f2) /. c).|| <= r
let c be Element of M; ::_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 Def1;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in X /\ (dom f1) by A7, XBOOLE_0:def_4;
then A10: |.(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 <= |.(f1 /. c).| & 0 <= ||.(f2 /. c).|| ) by CLVECT_1:105, COMPLEX1:46;
then  |.(f1 /. c).| * ||.(f2 /. c).|| <= r by A10, A12, XREAL_1:66;
then  ||.((f1 /. c) * (f2 /. c)).|| <= r by CLVECT_1:def_13;
hence  ||.((f1 (#) f2) /. c).|| <= r by A8, Def1; ::_thesis: verum
end;
hence  f1 (#) f2 is_bounded_on X /\ Y by Def3; ::_thesis: verum
end;

theorem :: VFUNCT_2:48
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X, Y being set 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 M,V; ::_thesis: for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let X, Y be set ; ::_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_2:49
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let f be PartFunc of M,V; ::_thesis: for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let X, Y be set ; ::_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 M st c in X /\ (dom f) holds
||.(f /. c).|| <= r1 by A1, Def3;
consider r2 being Real such that
A4: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= r2 by A2, Def3;
take r = (abs r1) + (abs r2); :: according to VFUNCT_2:def_3 ::_thesis: for x being Element of M st x in (X \/ Y) /\ (dom f) holds
||.(f /. x).|| <= r
let c be Element of M; ::_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_2:50
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant )
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X, Y being set st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant )
let f1, f2 be PartFunc of M,V; ::_thesis: for X, Y being set st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant )
let X, Y be set ; ::_thesis: ( f1 | X is constant & f2 | Y is constant implies ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant ) )
assume that
A1: f1 | X is constant and
A2: f2 | Y is constant ; ::_thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant )
consider r1 being VECTOR of V such that
A3: for c being Element of M 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 M st c in Y /\ (dom f2) holds
f2 /. c = r2 by A2, PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_
(f1_+_f2)_/._c_=_r1_+_r2
let c be Element of M; ::_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 VFUNCT_1:def_1;
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, VFUNCT_1:def_1
.= r1 + (f2 /. c) by A3, A10
.= r1 + r2 by A4, A12 ; ::_thesis: verum
end;
hence  (f1 + f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: (f1 - f2) | (X /\ Y) is constant
now__::_thesis:_for_c_being_Element_of_M_st_c_in_(X_/\_Y)_/\_(dom_(f1_-_f2))_holds_
(f1_-_f2)_/._c_=_r1_-_r2
let c be Element of M; ::_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 VFUNCT_1:def_2;
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, VFUNCT_1:def_2
.= r1 - (f2 /. c) by A3, A18
.= r1 - r2 by A4, A20 ; ::_thesis: verum
end;
hence  (f1 - f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem :: VFUNCT_2:51
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let V be ComplexNormSpace; ::_thesis: for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let f2 be PartFunc of M,V; ::_thesis: for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let X, Y be set ; ::_thesis: for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let f1 be PartFunc of M,COMPLEX; ::_thesis: ( f1 | X is constant & f2 | Y is constant implies (f1 (#) f2) | (X /\ Y) is constant )
assume that
A1: f1 | X is constant and
A2: f2 | Y is constant ; ::_thesis: (f1 (#) f2) | (X /\ Y) is constant
consider z1 being Element of COMPLEX  such that
A3: for c being Element of M st c in X /\ (dom f1) holds
f1 . c = z1 by A1, PARTFUN2:57;
consider r2 being VECTOR of V such that
A4: for c being Element of M st c in Y /\ (dom f2) holds
f2 /. c = r2 by A2, PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
(f1_(#)_f2)_/._c_=_z1_*_r2
let c be Element of M; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = z1 * r2 )
assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) /. c = z1 * r2
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 A10: c in dom f1 by XBOOLE_0:def_4;
then A11: f1 /. c = f1 . c by PARTFUN1:def_6;
 c in dom f2 by A9, XBOOLE_0:def_4;
then A12: c in Y /\ (dom f2) by A7, XBOOLE_0:def_4;
 c in X by A6, XBOOLE_0:def_4;
then A13: c in X /\ (dom f1) by A10, XBOOLE_0:def_4;
thus (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by A8, Def1
.= z1 * (f2 /. c) by A3, A13, A11
.= z1 * r2 by A4, A12 ; ::_thesis: verum
end;
hence  (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem Th52: :: VFUNCT_2:52
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let f be PartFunc of M,V; ::_thesis: for z being Element of COMPLEX
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let z be Element of COMPLEX ; ::_thesis: for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let Y be set ; ::_thesis: ( f | Y is constant implies (z (#) f) | Y is constant )
assume  f | Y is constant ; ::_thesis: (z (#) f) | Y is constant
then consider r being VECTOR of V such that
A1: for c being Element of M st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_Y_/\_(dom_(z_(#)_f))_holds_
(z_(#)_f)_/._c_=_z_*_r
let c be Element of M; ::_thesis: ( c in Y /\ (dom (z (#) f)) implies (z (#) f) /. c = z * r )
assume A2: c in Y /\ (dom (z (#) f)) ; ::_thesis: (z (#) f) /. c = z * r
then A3: c in Y by XBOOLE_0:def_4;
A4: c in dom (z (#) f) by A2, XBOOLE_0:def_4;
then  c in dom f by Def2;
then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4;
thus (z (#) f) /. c = z * (f /. c) by A4, Def2
.= z * r by A1, A5 ; ::_thesis: verum
end;
hence  (z (#) f) | Y is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem Th53: :: VFUNCT_2:53
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
let f be PartFunc of M,V; ::_thesis: for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
let Y be set ; ::_thesis: ( f | Y is constant implies ( ||.f.|| | Y is constant & (- f) | Y is constant ) )
assume  f | Y is constant ; ::_thesis: ( ||.f.|| | Y is constant & (- f) | Y is constant )
then consider r being VECTOR of V such that
A1: for c being Element of M st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_M_st_c_in_Y_/\_(dom_||.f.||)_holds_
||.f.||_._c_=_||.r.||
let c be Element of M; ::_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 constant by PARTFUN2:57; ::_thesis: (- f) | Y is constant
now__::_thesis:_ex_p_being_Element_of_the_U1_of_V_st_
for_c_being_Element_of_M_st_c_in_Y_/\_(dom_(-_f))_holds_
(-_f)_/._c_=_p
take p = - r; ::_thesis: for c being Element of M st c in Y /\ (dom (- f)) holds
(- f) /. c = p
let c be Element of M; ::_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 VFUNCT_1:def_5;
then A7: - (f /. c) = p by A1;
 c in dom (- f) by A6, XBOOLE_0:def_4;
hence  (- f) /. c = p by A7, VFUNCT_1:def_5; ::_thesis: verum
end;
hence  (- f) | Y is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem Th54: :: VFUNCT_2:54
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
f is_bounded_on Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
f is_bounded_on Y
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for Y being set st f | Y is constant holds
f is_bounded_on Y
let f be PartFunc of M,V; ::_thesis: for Y being set st f | Y is constant holds
f is_bounded_on Y
let Y be set ; ::_thesis: ( f | Y is constant implies f is_bounded_on Y )
assume  f | Y is constant ; ::_thesis: f is_bounded_on Y
then consider r being VECTOR of V such that
A1: for c being Element of M 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_M_st_c_in_Y_/\_(dom_f)_holds_
||.(f_/._c).||_<=_p
take p = ||.r.||; ::_thesis: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= p
let c be Element of M; ::_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 Def3; ::_thesis: verum
end;

theorem :: VFUNCT_2:55
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ( for z being Element of COMPLEX holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ( for z being Element of COMPLEX holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let V be ComplexNormSpace; ::_thesis: for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ( for z being Element of COMPLEX holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let f be PartFunc of M,V; ::_thesis: for Y being set st f | Y is constant holds
( ( for z being Element of COMPLEX holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let Y be set ; ::_thesis: ( f | Y is constant implies ( ( for z being Element of COMPLEX holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) )
assume A1: f | Y is constant ; ::_thesis: ( ( for z being Element of COMPLEX holds z (#) 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 z be Element of COMPLEX ; ::_thesis: z (#) f is_bounded_on Y
 (z (#) f) | Y is constant by A1, Th52;
hence  z (#) f is_bounded_on Y by Th54; ::_thesis: verum
end;
 (- f) | Y is constant by A1, Th53;
hence  - f is_bounded_on Y by Th54; ::_thesis: ||.f.|| | Y is bounded
 ||.f.|| | Y is constant by A1, Th53;
hence  ||.f.|| | Y is bounded ; ::_thesis: verum
end;

theorem :: VFUNCT_2:56
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
f1 + f2 is_bounded_on X /\ Y
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
f1 + f2 is_bounded_on X /\ Y
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
f1 + f2 is_bounded_on X /\ Y
let f1, f2 be PartFunc of M,V; ::_thesis: for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
f1 + f2 is_bounded_on X /\ Y
let X, Y be set ; ::_thesis: ( f1 is_bounded_on X & f2 | Y is constant implies f1 + f2 is_bounded_on X /\ Y )
assume that
A1: f1 is_bounded_on X and
A2: f2 | Y is constant ; ::_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_2:57
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
proof
let M be non empty set ; ::_thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
let V be ComplexNormSpace; ::_thesis: for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
let f1, f2 be PartFunc of M,V; ::_thesis: for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y )
let X, Y be set ; ::_thesis: ( f1 is_bounded_on X & f2 | Y is constant 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 constant ; ::_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;