:: 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;