:: VFUNCT_1 semantic presentation begin definition let C be non empty set ; let V be non empty addLoopStr ; let f1, f2 be PartFunc of C,V; deffunc H1( set ) -> Element of the U1 of V = (f1 /. \$1) + (f2 /. \$1); deffunc H2( set ) -> Element of the U1 of V = (f1 /. \$1) - (f2 /. \$1); defpred S1[ set ] means \$1 in (dom f1) /\ (dom f2); set X = (dom f1) /\ (dom f2); funcf1 + f2 -> PartFunc of C,V means :Def1: :: VFUNCT_1:def 1 ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds it /. c = (f1 /. c) + (f2 /. c) ) ); existence ex b1 being PartFunc of C,V st ( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 /. c) + (f2 /. c) ) ) proof consider F being PartFunc of C,V such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F /. c = (f1 /. c) + (f2 /. c) ) ) thus ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F /. c = (f1 /. c) + (f2 /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 /. c) + (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds b2 /. c = (f1 /. c) + (f2 /. c) ) holds b1 = b2 proof thus for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds f /. c = H1(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom g holds g /. c = H1(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; funcf1 - f2 -> PartFunc of C,V means :Def2: :: VFUNCT_1:def 2 ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds it /. c = (f1 /. c) - (f2 /. c) ) ); existence ex b1 being PartFunc of C,V st ( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 /. c) - (f2 /. c) ) ) proof consider F being PartFunc of C,V such that A3: for c being Element of C holds ( c in dom F iff S1[c] ) and A4: for c being Element of C st c in dom F holds F /. c = H2(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F /. c = (f1 /. c) - (f2 /. c) ) ) thus ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F /. c = (f1 /. c) - (f2 /. c) ) ) by A3, A4, SUBSET_1:3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 /. c) - (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds b2 /. c = (f1 /. c) - (f2 /. c) ) holds b1 = b2 proof thus for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds f /. c = H2(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom g holds g /. c = H2(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; end; :: deftheorem Def1 defines + VFUNCT_1:def_1_:_ for C being non empty set for V being non empty addLoopStr for f1, f2, b5 being PartFunc of C,V holds ( b5 = f1 + f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b5 holds b5 /. c = (f1 /. c) + (f2 /. c) ) ) ); :: deftheorem Def2 defines - VFUNCT_1:def_2_:_ for C being non empty set for V being non empty addLoopStr for f1, f2, b5 being PartFunc of C,V holds ( b5 = f1 - f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b5 holds b5 /. c = (f1 /. c) - (f2 /. c) ) ) ); registration let C be non empty set ; let V be non empty addLoopStr ; let f1, f2 be Function of C,V; clusterf1 + f2 -> total ; coherence f1 + f2 is total proof thus dom (f1 + f2) = (dom f1) /\ (dom f2) by Def1 .= C /\ (dom f2) by FUNCT_2:def_1 .= C /\ C by FUNCT_2:def_1 .= C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; clusterf1 - f2 -> total ; coherence f1 - f2 is total proof thus dom (f1 - f2) = (dom f1) /\ (dom f2) by Def2 .= C /\ (dom f2) by FUNCT_2:def_1 .= C /\ C by FUNCT_2:def_1 .= C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; definition let C be non empty set ; let V be non empty RLSStruct ; let f1 be PartFunc of C,REAL; let f2 be PartFunc of C,V; deffunc H1( Element of C) -> Element of the U1 of V = (f1 . \$1) * (f2 /. \$1); defpred S1[ set ] means \$1 in (dom f1) /\ (dom f2); set X = (dom f1) /\ (dom f2); funcf1 (#) f2 -> PartFunc of C,V means :Def3: :: VFUNCT_1:def 3 ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds it /. c = (f1 . c) * (f2 /. c) ) ); existence ex b1 being PartFunc of C,V st ( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 . c) * (f2 /. c) ) ) proof consider F being PartFunc of C,V such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F /. c = (f1 . c) * (f2 /. c) ) ) thus ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F /. c = (f1 . c) * (f2 /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 . c) * (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds b2 /. c = (f1 . c) * (f2 /. c) ) holds b1 = b2 proof thus for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds f /. c = H1(c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom g holds g /. c = H1(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; end; :: deftheorem Def3 defines (#) VFUNCT_1:def_3_:_ for C being non empty set for V being non empty RLSStruct for f1 being PartFunc of C,REAL for f2, b5 being PartFunc of C,V holds ( b5 = f1 (#) f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b5 holds b5 /. c = (f1 . c) * (f2 /. c) ) ) ); registration let C be non empty set ; let V be non empty RLSStruct ; let f1 be Function of C,REAL; let f2 be Function of C,V; clusterf1 (#) f2 -> total ; coherence f1 (#) f2 is total proof thus dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def3 .= C /\ (dom f2) by FUNCT_2:def_1 .= C /\ C by FUNCT_2:def_1 .= C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; definition let C be non empty set ; let V be non empty RLSStruct ; let f be PartFunc of C,V; let r be Real; deffunc H1( Element of C) -> Element of the U1 of V = r * (f /. \$1); defpred S1[ set ] means \$1 in dom f; funcr (#) f -> PartFunc of C,V means :Def4: :: VFUNCT_1:def 4 ( dom it = dom f & ( for c being Element of C st c in dom it holds it /. c = r * (f /. c) ) ); existence ex b1 being PartFunc of C,V st ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 /. c = r * (f /. c) ) ) proof consider F being PartFunc of C,V such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds F /. c = r * (f /. c) ) ) thus ( dom F = dom f & ( for c being Element of C st c in dom F holds F /. c = r * (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,V st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 /. c = r * (f /. c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds b2 /. c = r * (f /. c) ) holds b1 = b2 proof set X = dom f; thus for f, g being PartFunc of C,V st dom f = dom f & ( for c being Element of C st c in dom f holds f /. c = H1(c) ) & dom g = dom f & ( for c being Element of C st c in dom g holds g /. c = H1(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; end; :: deftheorem Def4 defines (#) VFUNCT_1:def_4_:_ for C being non empty set for V being non empty RLSStruct for f being PartFunc of C,V for r being Real for b5 being PartFunc of C,V holds ( b5 = r (#) f iff ( dom b5 = dom f & ( for c being Element of C st c in dom b5 holds b5 /. c = r * (f /. c) ) ) ); registration let C be non empty set ; let V be non empty RLSStruct ; let f be Function of C,V; let r be Real; clusterr (#) f -> total ; coherence r (#) f is total proof thus dom (r (#) f) = dom f by Def4 .= C by FUNCT_2:def_1 ; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; definition let C be non empty set ; let V be non empty addLoopStr ; let f be PartFunc of C,V; deffunc H1( Element of C) -> Element of the U1 of V = - (f /. \$1); defpred S1[ set ] means \$1 in dom f; func - f -> PartFunc of C,V means :Def5: :: VFUNCT_1:def 5 ( dom it = dom f & ( for c being Element of C st c in dom it holds it /. c = - (f /. c) ) ); existence ex b1 being PartFunc of C,V st ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 /. c = - (f /. c) ) ) proof consider F being PartFunc of C,V such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds F /. c = - (f /. c) ) ) thus ( dom F = dom f & ( for c being Element of C st c in dom F holds F /. c = - (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,V st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 /. c = - (f /. c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds b2 /. c = - (f /. c) ) holds b1 = b2 proof set X = dom f; thus for f, g being PartFunc of C,V st dom f = dom f & ( for c being Element of C st c in dom f holds f /. c = H1(c) ) & dom g = dom f & ( for c being Element of C st c in dom g holds g /. c = H1(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; end; :: deftheorem Def5 defines - VFUNCT_1:def_5_:_ for C being non empty set for V being non empty addLoopStr for f, b4 being PartFunc of C,V holds ( b4 = - f iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds b4 /. c = - (f /. c) ) ) ); registration let C be non empty set ; let V be non empty addLoopStr ; let f be Function of C,V; cluster - f -> total ; coherence - f is total proof thus dom (- f) = dom f by Def5 .= C by FUNCT_2:def_1 ; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; theorem :: VFUNCT_1:1 for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) let f1 be PartFunc of C,REAL; ::_thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) thus (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) c= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) :: according to XBOOLE_0:def_10 ::_thesis: ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) or x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) ) assume A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) ; ::_thesis: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) then A2: x in dom (f1 (#) f2) by XBOOLE_0:def_5; reconsider x1 = x as Element of C by A1; not x in (f1 (#) f2) " {(0. V)} by A1, XBOOLE_0:def_5; then not (f1 (#) f2) /. x1 in {(0. V)} by A2, PARTFUN2:26; then (f1 (#) f2) /. x1 <> 0. V by TARSKI:def_1; then A3: (f1 . x1) * (f2 /. x1) <> 0. V by A2, Def3; then f2 /. x1 <> 0. V by RLVECT_1:10; then not f2 /. x1 in {(0. V)} by TARSKI:def_1; then A4: not x1 in f2 " {(0. V)} by PARTFUN2:26; A5: x1 in (dom f1) /\ (dom f2) by A2, Def3; then x1 in dom f2 by XBOOLE_0:def_4; then A6: x in (dom f2) \ (f2 " {(0. V)}) by A4, XBOOLE_0:def_5; f1 . x1 <> 0 by A3, RLVECT_1:10; then not f1 . x1 in {0} by TARSKI:def_1; then A7: not x1 in f1 " {0} by FUNCT_1:def_7; x1 in dom f1 by A5, XBOOLE_0:def_4; then x in (dom f1) \ (f1 " {0}) by A7, XBOOLE_0:def_5; hence x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) by A6, XBOOLE_0:def_4; ::_thesis: verum end; thus ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) ) assume A8: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)})) ; ::_thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) then reconsider x1 = x as Element of C ; A9: x in (dom f2) \ (f2 " {(0. V)}) by A8, XBOOLE_0:def_4; then A10: x in dom f2 by XBOOLE_0:def_5; not x in f2 " {(0. V)} by A9, XBOOLE_0:def_5; then not f2 /. x1 in {(0. V)} by A10, PARTFUN2:26; then A11: f2 /. x1 <> 0. V by TARSKI:def_1; A12: x in (dom f1) \ (f1 " {0}) by A8, XBOOLE_0:def_4; then A13: x in dom f1 by XBOOLE_0:def_5; then x1 in (dom f1) /\ (dom f2) by A10, XBOOLE_0:def_4; then A14: x1 in dom (f1 (#) f2) by Def3; not x in f1 " {0} by A12, XBOOLE_0:def_5; then not f1 . x1 in {0} by A13, FUNCT_1:def_7; then f1 . x1 <> 0 by TARSKI:def_1; then (f1 . x1) * (f2 /. x1) <> 0. V by A11, RLVECT_1:11; then (f1 (#) f2) /. x1 <> 0. V by A14, Def3; then not (f1 (#) f2) /. x1 in {(0. V)} by TARSKI:def_1; then not x in (f1 (#) f2) " {(0. V)} by PARTFUN2:26; hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) by A14, XBOOLE_0:def_5; ::_thesis: verum end; end; theorem :: VFUNCT_1:2 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} ) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} ) let f be PartFunc of C,V; ::_thesis: ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} ) now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_||.f.||_"_{0}_implies_c_in_f_"_{(0._V)}_)_&_(_c_in_f_"_{(0._V)}_implies_c_in_||.f.||_"_{0}_)_) let c be Element of C; ::_thesis: ( ( c in ||.f.|| " {0} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in ||.f.|| " {0} ) ) thus ( c in ||.f.|| " {0} implies c in f " {(0. V)} ) ::_thesis: ( c in f " {(0. V)} implies c in ||.f.|| " {0} ) proof assume A1: c in ||.f.|| " {0} ; ::_thesis: c in f " {(0. V)} then A2: c in dom ||.f.|| by FUNCT_1:def_7; ||.f.|| . c in {0} by A1, FUNCT_1:def_7; then ||.f.|| . c = 0 by TARSKI:def_1; then ||.(f /. c).|| = 0 by A2, NORMSP_0:def_3; then f /. c = 0. V by NORMSP_0:def_5; then A3: f /. c in {(0. V)} by TARSKI:def_1; c in dom f by A2, NORMSP_0:def_3; hence c in f " {(0. V)} by A3, PARTFUN2:26; ::_thesis: verum end; assume A4: c in f " {(0. V)} ; ::_thesis: c in ||.f.|| " {0} then c in dom f by PARTFUN2:26; then A5: c in dom ||.f.|| by NORMSP_0:def_3; f /. c in {(0. V)} by A4, PARTFUN2:26; then f /. c = 0. V by TARSKI:def_1; then ||.(f /. c).|| = 0 ; then ||.f.|| . c = 0 by A5, NORMSP_0:def_3; then ||.f.|| . c in {0} by TARSKI:def_1; hence c in ||.f.|| " {0} by A5, FUNCT_1:def_7; ::_thesis: verum end; hence ||.f.|| " {0} = f " {(0. V)} by SUBSET_1:3; ::_thesis: (- f) " {(0. V)} = f " {(0. V)} now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_(-_f)_"_{(0._V)}_implies_c_in_f_"_{(0._V)}_)_&_(_c_in_f_"_{(0._V)}_implies_c_in_(-_f)_"_{(0._V)}_)_) let c be Element of C; ::_thesis: ( ( c in (- f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (- f) " {(0. V)} ) ) thus ( c in (- f) " {(0. V)} implies c in f " {(0. V)} ) ::_thesis: ( c in f " {(0. V)} implies c in (- f) " {(0. V)} ) proof assume A6: c in (- f) " {(0. V)} ; ::_thesis: c in f " {(0. V)} then A7: c in dom (- f) by PARTFUN2:26; (- f) /. c in {(0. V)} by A6, PARTFUN2:26; then (- f) /. c = 0. V by TARSKI:def_1; then - (- (f /. c)) = - (0. V) by A7, Def5; then - (- (f /. c)) = 0. V by RLVECT_1:12; then f /. c = 0. V by RLVECT_1:17; then A8: f /. c in {(0. V)} by TARSKI:def_1; c in dom f by A7, Def5; hence c in f " {(0. V)} by A8, PARTFUN2:26; ::_thesis: verum end; assume A9: c in f " {(0. V)} ; ::_thesis: c in (- f) " {(0. V)} then c in dom f by PARTFUN2:26; then A10: c in dom (- f) by Def5; f /. c in {(0. V)} by A9, PARTFUN2:26; then f /. c = 0. V by TARSKI:def_1; then (- f) /. c = - (0. V) by A10, Def5; then (- f) /. c = 0. V by RLVECT_1:12; then (- f) /. c in {(0. V)} by TARSKI:def_1; hence c in (- f) " {(0. V)} by A10, PARTFUN2:26; ::_thesis: verum end; hence (- f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; ::_thesis: verum end; theorem :: VFUNCT_1:3 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real st r <> 0 holds (r (#) f) " {(0. V)} = f " {(0. V)} proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r being Real st r <> 0 holds (r (#) f) " {(0. V)} = f " {(0. V)} let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r being Real st r <> 0 holds (r (#) f) " {(0. V)} = f " {(0. V)} let f be PartFunc of C,V; ::_thesis: for r being Real st r <> 0 holds (r (#) f) " {(0. V)} = f " {(0. V)} let r be Real; ::_thesis: ( r <> 0 implies (r (#) f) " {(0. V)} = f " {(0. V)} ) assume A1: r <> 0 ; ::_thesis: (r (#) f) " {(0. V)} = f " {(0. V)} now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_(r_(#)_f)_"_{(0._V)}_implies_c_in_f_"_{(0._V)}_)_&_(_c_in_f_"_{(0._V)}_implies_c_in_(r_(#)_f)_"_{(0._V)}_)_) let c be Element of C; ::_thesis: ( ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} ) ) thus ( c in (r (#) f) " {(0. V)} implies c in f " {(0. V)} ) ::_thesis: ( c in f " {(0. V)} implies c in (r (#) f) " {(0. V)} ) proof assume A2: c in (r (#) f) " {(0. V)} ; ::_thesis: c in f " {(0. V)} then A3: c in dom (r (#) f) by PARTFUN2:26; (r (#) f) /. c in {(0. V)} by A2, PARTFUN2:26; then (r (#) f) /. c = 0. V by TARSKI:def_1; then r * (f /. c) = 0. V by A3, Def4; then r * (f /. c) = r * (0. V) by RLVECT_1:10; then f /. c = 0. V by A1, RLVECT_1:36; then A4: f /. c in {(0. V)} by TARSKI:def_1; c in dom f by A3, Def4; hence c in f " {(0. V)} by A4, PARTFUN2:26; ::_thesis: verum end; assume A5: c in f " {(0. V)} ; ::_thesis: c in (r (#) f) " {(0. V)} then c in dom f by PARTFUN2:26; then A6: c in dom (r (#) f) by Def4; f /. c in {(0. V)} by A5, PARTFUN2:26; then r * (f /. c) = r * (0. V) by TARSKI:def_1; then r * (f /. c) = 0. V by RLVECT_1:10; then (r (#) f) /. c = 0. V by A6, Def4; then (r (#) f) /. c in {(0. V)} by TARSKI:def_1; hence c in (r (#) f) " {(0. V)} by A6, PARTFUN2:26; ::_thesis: verum end; hence (r (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; ::_thesis: verum end; theorem Th4: :: VFUNCT_1:4 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 let f1, f2 be PartFunc of C,V; ::_thesis: f1 + f2 = f2 + f1 A1: dom (f1 + f2) = (dom f2) /\ (dom f1) by Def1 .= dom (f2 + f1) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_/._c_=_(f2_+_f1)_/._c let c be Element of C; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) /. c = (f2 + f1) /. c ) assume A2: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) /. c = (f2 + f1) /. c hence (f1 + f2) /. c = (f2 /. c) + (f1 /. c) by Def1 .= (f2 + f1) /. c by A1, A2, Def1 ; ::_thesis: verum end; hence f1 + f2 = f2 + f1 by A1, PARTFUN2:1; ::_thesis: verum end; definition let C be non empty set ; let V be RealNormSpace; let f1, f2 be PartFunc of C,V; :: original: + redefine funcf1 + f2 -> PartFunc of C,V; commutativity for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 by Th4; end; theorem :: VFUNCT_1:5 for C being non empty set for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3) let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3) let f1, f2, f3 be PartFunc of C,V; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3) A1: dom ((f1 + f2) + f3) = (dom (f1 + f2)) /\ (dom f3) by Def1 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by Def1 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 + f3)) by Def1 .= dom (f1 + (f2 + f3)) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_+_f3)_holds_ ((f1_+_f2)_+_f3)_/._c_=_(f1_+_(f2_+_f3))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) /. c = (f1 + (f2 + f3)) /. c ) assume A2: c in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) /. c = (f1 + (f2 + f3)) /. c then c in (dom (f1 + f2)) /\ (dom f3) by Def1; then A3: c in dom (f1 + f2) by XBOOLE_0:def_4; c in (dom f1) /\ (dom (f2 + f3)) by A1, A2, Def1; then A4: c in dom (f2 + f3) by XBOOLE_0:def_4; thus ((f1 + f2) + f3) /. c = ((f1 + f2) /. c) + (f3 /. c) by A2, Def1 .= ((f1 /. c) + (f2 /. c)) + (f3 /. c) by A3, Def1 .= (f1 /. c) + ((f2 /. c) + (f3 /. c)) by RLVECT_1:def_3 .= (f1 /. c) + ((f2 + f3) /. c) by A4, Def1 .= (f1 + (f2 + f3)) /. c by A1, A2, Def1 ; ::_thesis: verum end; hence (f1 + f2) + f3 = f1 + (f2 + f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:6 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,REAL for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,REAL for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,REAL for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) let f1, f2 be PartFunc of C,REAL; ::_thesis: for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) let f3 be PartFunc of C,V; ::_thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) A1: dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by Def3 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def_4 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 (#) f3)) by Def3 .= dom (f1 (#) (f2 (#) f3)) by Def3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_(#)_f3)_holds_ ((f1_(#)_f2)_(#)_f3)_/._c_=_(f1_(#)_(f2_(#)_f3))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) /. c = (f1 (#) (f2 (#) f3)) /. c ) assume A2: c in dom ((f1 (#) f2) (#) f3) ; ::_thesis: ((f1 (#) f2) (#) f3) /. c = (f1 (#) (f2 (#) f3)) /. c then c in (dom f1) /\ (dom (f2 (#) f3)) by A1, Def3; then A3: c in dom (f2 (#) f3) by XBOOLE_0:def_4; thus ((f1 (#) f2) (#) f3) /. c = ((f1 (#) f2) . c) * (f3 /. c) by A2, Def3 .= ((f1 . c) * (f2 . c)) * (f3 /. c) by VALUED_1:5 .= (f1 . c) * ((f2 . c) * (f3 /. c)) by RLVECT_1:def_7 .= (f1 . c) * ((f2 (#) f3) /. c) by A3, Def3 .= (f1 (#) (f2 (#) f3)) /. c by A1, A2, Def3 ; ::_thesis: verum end; hence (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:7 for C being non empty set for V being RealNormSpace for f3 being PartFunc of C,V for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f3 being PartFunc of C,V for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) let V be RealNormSpace; ::_thesis: for f3 being PartFunc of C,V for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) let f3 be PartFunc of C,V; ::_thesis: for f1, f2 being PartFunc of C,REAL holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) let f1, f2 be PartFunc of C,REAL; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by Def3 .= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:def_1 .= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16 .= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by Def3 .= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Def3 .= dom ((f1 (#) f3) + (f2 (#) f3)) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_(#)_f3)_holds_ ((f1_+_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_+_(f2_(#)_f3))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) (#) f3) implies ((f1 + f2) (#) f3) /. c = ((f1 (#) f3) + (f2 (#) f3)) /. c ) assume A2: c in dom ((f1 + f2) (#) f3) ; ::_thesis: ((f1 + f2) (#) f3) /. c = ((f1 (#) f3) + (f2 (#) f3)) /. c then c in (dom (f1 + f2)) /\ (dom f3) by Def3; then A3: c in dom (f1 + f2) by XBOOLE_0:def_4; A4: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, A2, Def1; then A5: c in dom (f1 (#) f3) by XBOOLE_0:def_4; A6: c in dom (f2 (#) f3) by A4, XBOOLE_0:def_4; thus ((f1 + f2) (#) f3) /. c = ((f1 + f2) . c) * (f3 /. c) by A2, Def3 .= ((f1 . c) + (f2 . c)) * (f3 /. c) by A3, VALUED_1:def_1 .= ((f1 . c) * (f3 /. c)) + ((f2 . c) * (f3 /. c)) by RLVECT_1:def_6 .= ((f1 (#) f3) /. c) + ((f2 . c) * (f3 /. c)) by A5, Def3 .= ((f1 (#) f3) /. c) + ((f2 (#) f3) /. c) by A6, Def3 .= ((f1 (#) f3) + (f2 (#) f3)) /. c by A1, A2, Def1 ; ::_thesis: verum end; hence (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:8 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) let f1, f2 be PartFunc of C,V; ::_thesis: for f3 being PartFunc of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) let f3 be PartFunc of C,REAL; ::_thesis: f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) A1: dom (f3 (#) (f1 + f2)) = (dom f3) /\ (dom (f1 + f2)) by Def3 .= (dom f3) /\ ((dom f1) /\ (dom f2)) by Def1 .= (((dom f3) /\ (dom f3)) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16 .= (((dom f3) /\ (dom f1)) /\ (dom f3)) /\ (dom f2) by XBOOLE_1:16 .= ((dom f3) /\ (dom f1)) /\ ((dom f3) /\ (dom f2)) by XBOOLE_1:16 .= (dom (f3 (#) f1)) /\ ((dom f3) /\ (dom f2)) by Def3 .= (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by Def3 .= dom ((f3 (#) f1) + (f3 (#) f2)) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f3_(#)_(f1_+_f2))_holds_ (f3_(#)_(f1_+_f2))_/._c_=_((f3_(#)_f1)_+_(f3_(#)_f2))_/._c let c be Element of C; ::_thesis: ( c in dom (f3 (#) (f1 + f2)) implies (f3 (#) (f1 + f2)) /. c = ((f3 (#) f1) + (f3 (#) f2)) /. c ) assume A2: c in dom (f3 (#) (f1 + f2)) ; ::_thesis: (f3 (#) (f1 + f2)) /. c = ((f3 (#) f1) + (f3 (#) f2)) /. c then c in (dom f3) /\ (dom (f1 + f2)) by Def3; then A3: c in dom (f1 + f2) by XBOOLE_0:def_4; A4: c in (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by A1, A2, Def1; then A5: c in dom (f3 (#) f1) by XBOOLE_0:def_4; A6: c in dom (f3 (#) f2) by A4, XBOOLE_0:def_4; thus (f3 (#) (f1 + f2)) /. c = (f3 . c) * ((f1 + f2) /. c) by A2, Def3 .= (f3 . c) * ((f1 /. c) + (f2 /. c)) by A3, Def1 .= ((f3 . c) * (f1 /. c)) + ((f3 . c) * (f2 /. c)) by RLVECT_1:def_5 .= ((f3 (#) f1) /. c) + ((f3 . c) * (f2 /. c)) by A5, Def3 .= ((f3 (#) f1) /. c) + ((f3 (#) f2) /. c) by A6, Def3 .= ((f3 (#) f1) + (f3 (#) f2)) /. c by A1, A2, Def1 ; ::_thesis: verum end; hence f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:9 for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let f2 be PartFunc of C,V; ::_thesis: for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let r be Real; ::_thesis: for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let f1 be PartFunc of C,REAL; ::_thesis: r (#) (f1 (#) f2) = (r (#) f1) (#) f2 A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Def4 .= (dom f1) /\ (dom f2) by Def3 .= (dom (r (#) f1)) /\ (dom f2) by VALUED_1:def_5 .= dom ((r (#) f1) (#) f2) by Def3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_ (r_(#)_(f1_(#)_f2))_/._c_=_((r_(#)_f1)_(#)_f2)_/._c let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) /. c = ((r (#) f1) (#) f2) /. c ) assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) /. c = ((r (#) f1) (#) f2) /. c then A3: c in dom (f1 (#) f2) by Def4; c in (dom (r (#) f1)) /\ (dom f2) by A1, A2, Def3; then A4: c in dom (r (#) f1) by XBOOLE_0:def_4; thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Def4 .= r * ((f1 . c) * (f2 /. c)) by A3, Def3 .= (r * (f1 . c)) * (f2 /. c) by RLVECT_1:def_7 .= ((r (#) f1) . c) * (f2 /. c) by A4, VALUED_1:def_5 .= ((r (#) f1) (#) f2) /. c by A1, A2, Def3 ; ::_thesis: verum end; hence r (#) (f1 (#) f2) = (r (#) f1) (#) f2 by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:10 for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let f2 be PartFunc of C,V; ::_thesis: for r being Real for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let r be Real; ::_thesis: for f1 being PartFunc of C,REAL holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let f1 be PartFunc of C,REAL; ::_thesis: r (#) (f1 (#) f2) = f1 (#) (r (#) f2) A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Def4 .= (dom f1) /\ (dom f2) by Def3 .= (dom f1) /\ (dom (r (#) f2)) by Def4 .= dom (f1 (#) (r (#) f2)) by Def3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_ (r_(#)_(f1_(#)_f2))_/._c_=_(f1_(#)_(r_(#)_f2))_/._c let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) /. c = (f1 (#) (r (#) f2)) /. c ) assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) /. c = (f1 (#) (r (#) f2)) /. c then A3: c in dom (f1 (#) f2) by Def4; c in (dom f1) /\ (dom (r (#) f2)) by A1, A2, Def3; then A4: c in dom (r (#) f2) by XBOOLE_0:def_4; thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Def4 .= r * ((f1 . c) * (f2 /. c)) by A3, Def3 .= ((f1 . c) * r) * (f2 /. c) by RLVECT_1:def_7 .= (f1 . c) * (r * (f2 /. c)) by RLVECT_1:def_7 .= (f1 . c) * ((r (#) f2) /. c) by A4, Def4 .= (f1 (#) (r (#) f2)) /. c by A1, A2, Def3 ; ::_thesis: verum end; hence r (#) (f1 (#) f2) = f1 (#) (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:11 for C being non empty set for V being RealNormSpace for f3 being PartFunc of C,V for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f3 being PartFunc of C,V for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) let V be RealNormSpace; ::_thesis: for f3 being PartFunc of C,V for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) let f3 be PartFunc of C,V; ::_thesis: for f1, f2 being PartFunc of C,REAL holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) let f1, f2 be PartFunc of C,REAL; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) A1: dom ((f1 - f2) (#) f3) = (dom (f1 - f2)) /\ (dom f3) by Def3 .= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:12 .= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16 .= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by Def3 .= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Def3 .= dom ((f1 (#) f3) - (f2 (#) f3)) by Def2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_-_f2)_(#)_f3)_holds_ ((f1_-_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_-_(f2_(#)_f3))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 - f2) (#) f3) implies ((f1 - f2) (#) f3) /. c = ((f1 (#) f3) - (f2 (#) f3)) /. c ) assume A2: c in dom ((f1 - f2) (#) f3) ; ::_thesis: ((f1 - f2) (#) f3) /. c = ((f1 (#) f3) - (f2 (#) f3)) /. c then c in (dom (f1 - f2)) /\ (dom f3) by Def3; then A3: c in dom (f1 - f2) by XBOOLE_0:def_4; A4: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, A2, Def2; then A5: c in dom (f1 (#) f3) by XBOOLE_0:def_4; A6: c in dom (f2 (#) f3) by A4, XBOOLE_0:def_4; thus ((f1 - f2) (#) f3) /. c = ((f1 - f2) . c) * (f3 /. c) by A2, Def3 .= ((f1 . c) - (f2 . c)) * (f3 /. c) by A3, VALUED_1:13 .= ((f1 . c) * (f3 /. c)) - ((f2 . c) * (f3 /. c)) by RLVECT_1:35 .= ((f1 (#) f3) /. c) - ((f2 . c) * (f3 /. c)) by A5, Def3 .= ((f1 (#) f3) /. c) - ((f2 (#) f3) /. c) by A6, Def3 .= ((f1 (#) f3) - (f2 (#) f3)) /. c by A1, A2, Def2 ; ::_thesis: verum end; hence (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:12 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) let f1, f2 be PartFunc of C,V; ::_thesis: for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) let f3 be PartFunc of C,REAL; ::_thesis: (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) A1: dom ((f3 (#) f1) - (f3 (#) f2)) = (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by Def2 .= (dom (f3 (#) f1)) /\ ((dom f3) /\ (dom f2)) by Def3 .= ((dom f3) /\ (dom f1)) /\ ((dom f3) /\ (dom f2)) by Def3 .= ((dom f3) /\ ((dom f3) /\ (dom f1))) /\ (dom f2) by XBOOLE_1:16 .= (((dom f3) /\ (dom f3)) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16 .= (dom f3) /\ ((dom f1) /\ (dom f2)) by XBOOLE_1:16 .= (dom f3) /\ (dom (f1 - f2)) by Def2 .= dom (f3 (#) (f1 - f2)) by Def3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f3_(#)_(f1_-_f2))_holds_ (f3_(#)_(f1_-_f2))_/._c_=_((f3_(#)_f1)_-_(f3_(#)_f2))_/._c let c be Element of C; ::_thesis: ( c in dom (f3 (#) (f1 - f2)) implies (f3 (#) (f1 - f2)) /. c = ((f3 (#) f1) - (f3 (#) f2)) /. c ) assume A2: c in dom (f3 (#) (f1 - f2)) ; ::_thesis: (f3 (#) (f1 - f2)) /. c = ((f3 (#) f1) - (f3 (#) f2)) /. c then c in (dom f3) /\ (dom (f1 - f2)) by Def3; then A3: c in dom (f1 - f2) by XBOOLE_0:def_4; A4: c in (dom (f3 (#) f1)) /\ (dom (f3 (#) f2)) by A1, A2, Def2; then A5: c in dom (f3 (#) f1) by XBOOLE_0:def_4; A6: c in dom (f3 (#) f2) by A4, XBOOLE_0:def_4; thus (f3 (#) (f1 - f2)) /. c = (f3 . c) * ((f1 - f2) /. c) by A2, Def3 .= (f3 . c) * ((f1 /. c) - (f2 /. c)) by A3, Def2 .= ((f3 . c) * (f1 /. c)) - ((f3 . c) * (f2 /. c)) by RLVECT_1:34 .= ((f3 (#) f1) /. c) - ((f3 . c) * (f2 /. c)) by A5, Def3 .= ((f3 (#) f1) /. c) - ((f3 (#) f2) /. c) by A6, Def3 .= ((f3 (#) f1) - (f3 (#) f2)) /. c by A1, A2, Def2 ; ::_thesis: verum end; hence (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:13 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) let f1, f2 be PartFunc of C,V; ::_thesis: for r being Real holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) let r be Real; ::_thesis: r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) A1: dom (r (#) (f1 + f2)) = dom (f1 + f2) by Def4 .= (dom f1) /\ (dom f2) by Def1 .= (dom f1) /\ (dom (r (#) f2)) by Def4 .= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Def4 .= dom ((r (#) f1) + (r (#) f2)) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_+_f2))_holds_ (r_(#)_(f1_+_f2))_/._c_=_((r_(#)_f1)_+_(r_(#)_f2))_/._c let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 + f2)) implies (r (#) (f1 + f2)) /. c = ((r (#) f1) + (r (#) f2)) /. c ) assume A2: c in dom (r (#) (f1 + f2)) ; ::_thesis: (r (#) (f1 + f2)) /. c = ((r (#) f1) + (r (#) f2)) /. c then A3: c in dom (f1 + f2) by Def4; A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, Def1; then A5: c in dom (r (#) f1) by XBOOLE_0:def_4; A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4; thus (r (#) (f1 + f2)) /. c = r * ((f1 + f2) /. c) by A2, Def4 .= r * ((f1 /. c) + (f2 /. c)) by A3, Def1 .= (r * (f1 /. c)) + (r * (f2 /. c)) by RLVECT_1:def_5 .= ((r (#) f1) /. c) + (r * (f2 /. c)) by A5, Def4 .= ((r (#) f1) /. c) + ((r (#) f2) /. c) by A6, Def4 .= ((r (#) f1) + (r (#) f2)) /. c by A1, A2, Def1 ; ::_thesis: verum end; hence r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th14: :: VFUNCT_1:14 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r, p being Real holds (r * p) (#) f = r (#) (p (#) f) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r, p being Real holds (r * p) (#) f = r (#) (p (#) f) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r, p being Real holds (r * p) (#) f = r (#) (p (#) f) let f be PartFunc of C,V; ::_thesis: for r, p being Real holds (r * p) (#) f = r (#) (p (#) f) let r, p be Real; ::_thesis: (r * p) (#) f = r (#) (p (#) f) A1: dom ((r * p) (#) f) = dom f by Def4 .= dom (p (#) f) by Def4 .= dom (r (#) (p (#) f)) by Def4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_*_p)_(#)_f)_holds_ ((r_*_p)_(#)_f)_/._c_=_(r_(#)_(p_(#)_f))_/._c let c be Element of C; ::_thesis: ( c in dom ((r * p) (#) f) implies ((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c ) assume A2: c in dom ((r * p) (#) f) ; ::_thesis: ((r * p) (#) f) /. c = (r (#) (p (#) f)) /. c then A3: c in dom (p (#) f) by A1, Def4; thus ((r * p) (#) f) /. c = (r * p) * (f /. c) by A2, Def4 .= r * (p * (f /. c)) by RLVECT_1:def_7 .= r * ((p (#) f) /. c) by A3, Def4 .= (r (#) (p (#) f)) /. c by A1, A2, Def4 ; ::_thesis: verum end; hence (r * p) (#) f = r (#) (p (#) f) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:15 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) let f1, f2 be PartFunc of C,V; ::_thesis: for r being Real holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) let r be Real; ::_thesis: r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) A1: dom (r (#) (f1 - f2)) = dom (f1 - f2) by Def4 .= (dom f1) /\ (dom f2) by Def2 .= (dom f1) /\ (dom (r (#) f2)) by Def4 .= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Def4 .= dom ((r (#) f1) - (r (#) f2)) by Def2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_-_f2))_holds_ (r_(#)_(f1_-_f2))_/._c_=_((r_(#)_f1)_-_(r_(#)_f2))_/._c let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 - f2)) implies (r (#) (f1 - f2)) /. c = ((r (#) f1) - (r (#) f2)) /. c ) assume A2: c in dom (r (#) (f1 - f2)) ; ::_thesis: (r (#) (f1 - f2)) /. c = ((r (#) f1) - (r (#) f2)) /. c then A3: c in dom (f1 - f2) by Def4; A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, Def2; then A5: c in dom (r (#) f1) by XBOOLE_0:def_4; A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4; thus (r (#) (f1 - f2)) /. c = r * ((f1 - f2) /. c) by A2, Def4 .= r * ((f1 /. c) - (f2 /. c)) by A3, Def2 .= (r * (f1 /. c)) - (r * (f2 /. c)) by RLVECT_1:34 .= ((r (#) f1) /. c) - (r * (f2 /. c)) by A5, Def4 .= ((r (#) f1) /. c) - ((r (#) f2) /. c) by A6, Def4 .= ((r (#) f1) - (r (#) f2)) /. c by A1, A2, Def2 ; ::_thesis: verum end; hence r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:16 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1) let f1, f2 be PartFunc of C,V; ::_thesis: f1 - f2 = (- 1) (#) (f2 - f1) A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by Def2 .= dom (f2 - f1) by Def2 .= dom ((- 1) (#) (f2 - f1)) by Def4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_/._c_=_((-_1)_(#)_(f2_-_f1))_/._c A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by Def2 .= dom (f2 - f1) by Def2 ; let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = ((- 1) (#) (f2 - f1)) /. c ) assume A3: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. c = ((- 1) (#) (f2 - f1)) /. c thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A3, Def2 .= - ((f2 /. c) - (f1 /. c)) by RLVECT_1:33 .= (- 1) * ((f2 /. c) - (f1 /. c)) by RLVECT_1:16 .= (- 1) * ((f2 - f1) /. c) by A3, A2, Def2 .= ((- 1) (#) (f2 - f1)) /. c by A1, A3, Def4 ; ::_thesis: verum end; hence f1 - f2 = (- 1) (#) (f2 - f1) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:17 for C being non empty set for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3 proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3 let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3 let f1, f2, f3 be PartFunc of C,V; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3 A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by Def2 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by Def1 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 - f2)) /\ (dom f3) by Def2 .= dom ((f1 - f2) - f3) by Def2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_+_f3))_holds_ (f1_-_(f2_+_f3))_/._c_=_((f1_-_f2)_-_f3)_/._c let c be Element of C; ::_thesis: ( c in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) /. c = ((f1 - f2) - f3) /. c ) assume A2: c in dom (f1 - (f2 + f3)) ; ::_thesis: (f1 - (f2 + f3)) /. c = ((f1 - f2) - f3) /. c then c in (dom f1) /\ (dom (f2 + f3)) by Def2; then A3: c in dom (f2 + f3) by XBOOLE_0:def_4; c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, Def2; then A4: c in dom (f1 - f2) by XBOOLE_0:def_4; thus (f1 - (f2 + f3)) /. c = (f1 /. c) - ((f2 + f3) /. c) by A2, Def2 .= (f1 /. c) - ((f2 /. c) + (f3 /. c)) by A3, Def1 .= ((f1 /. c) - (f2 /. c)) - (f3 /. c) by RLVECT_1:27 .= ((f1 - f2) /. c) - (f3 /. c) by A4, Def2 .= ((f1 - f2) - f3) /. c by A1, A2, Def2 ; ::_thesis: verum end; hence f1 - (f2 + f3) = (f1 - f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th18: :: VFUNCT_1:18 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds 1 (#) f = f proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds 1 (#) f = f let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds 1 (#) f = f let f be PartFunc of C,V; ::_thesis: 1 (#) f = f A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(1_(#)_f)_holds_ (1_(#)_f)_/._c_=_f_/._c let c be Element of C; ::_thesis: ( c in dom (1 (#) f) implies (1 (#) f) /. c = f /. c ) assume c in dom (1 (#) f) ; ::_thesis: (1 (#) f) /. c = f /. c hence (1 (#) f) /. c = 1 * (f /. c) by Def4 .= f /. c by RLVECT_1:def_8 ; ::_thesis: verum end; dom (1 (#) f) = dom f by Def4; hence 1 (#) f = f by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:19 for C being non empty set for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3 proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3 let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3 let f1, f2, f3 be PartFunc of C,V; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3 A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by Def2 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by Def2 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 - f2)) /\ (dom f3) by Def2 .= dom ((f1 - f2) + f3) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_-_f3))_holds_ (f1_-_(f2_-_f3))_/._c_=_((f1_-_f2)_+_f3)_/._c let c be Element of C; ::_thesis: ( c in dom (f1 - (f2 - f3)) implies (f1 - (f2 - f3)) /. c = ((f1 - f2) + f3) /. c ) assume A2: c in dom (f1 - (f2 - f3)) ; ::_thesis: (f1 - (f2 - f3)) /. c = ((f1 - f2) + f3) /. c then c in (dom f1) /\ (dom (f2 - f3)) by Def2; then A3: c in dom (f2 - f3) by XBOOLE_0:def_4; c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, Def1; then A4: c in dom (f1 - f2) by XBOOLE_0:def_4; thus (f1 - (f2 - f3)) /. c = (f1 /. c) - ((f2 - f3) /. c) by A2, Def2 .= (f1 /. c) - ((f2 /. c) - (f3 /. c)) by A3, Def2 .= ((f1 /. c) - (f2 /. c)) + (f3 /. c) by RLVECT_1:29 .= ((f1 - f2) /. c) + (f3 /. c) by A4, Def2 .= ((f1 - f2) + f3) /. c by A1, A2, Def1 ; ::_thesis: verum end; hence f1 - (f2 - f3) = (f1 - f2) + f3 by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:20 for C being non empty set for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3 proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3 let V be RealNormSpace; ::_thesis: for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3 let f1, f2, f3 be PartFunc of C,V; ::_thesis: f1 + (f2 - f3) = (f1 + f2) - f3 A1: dom (f1 + (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by Def1 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by Def2 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 + f2)) /\ (dom f3) by Def1 .= dom ((f1 + f2) - f3) by Def2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_(f2_-_f3))_holds_ (f1_+_(f2_-_f3))_/._c_=_((f1_+_f2)_-_f3)_/._c let c be Element of C; ::_thesis: ( c in dom (f1 + (f2 - f3)) implies (f1 + (f2 - f3)) /. c = ((f1 + f2) - f3) /. c ) assume A2: c in dom (f1 + (f2 - f3)) ; ::_thesis: (f1 + (f2 - f3)) /. c = ((f1 + f2) - f3) /. c then c in (dom f1) /\ (dom (f2 - f3)) by Def1; then A3: c in dom (f2 - f3) by XBOOLE_0:def_4; c in (dom (f1 + f2)) /\ (dom f3) by A1, A2, Def2; then A4: c in dom (f1 + f2) by XBOOLE_0:def_4; thus (f1 + (f2 - f3)) /. c = (f1 /. c) + ((f2 - f3) /. c) by A2, Def1 .= (f1 /. c) + ((f2 /. c) - (f3 /. c)) by A3, Def2 .= ((f1 /. c) + (f2 /. c)) - (f3 /. c) by RLVECT_1:def_3 .= ((f1 + f2) /. c) - (f3 /. c) by A4, Def1 .= ((f1 + f2) - f3) /. c by A1, A2, Def2 ; ::_thesis: verum end; hence f1 + (f2 - f3) = (f1 + f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:21 for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| let f1 be PartFunc of C,REAL; ::_thesis: ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| A1: dom ||.(f1 (#) f2).|| = dom (f1 (#) f2) by NORMSP_0:def_3 .= (dom f1) /\ (dom f2) by Def3 .= (dom f1) /\ (dom ||.f2.||) by NORMSP_0:def_3 .= (dom (abs f1)) /\ (dom ||.f2.||) by VALUED_1:def_11 .= dom ((abs f1) (#) ||.f2.||) by VALUED_1:def_4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_||.(f1_(#)_f2).||_holds_ ||.(f1_(#)_f2).||_._c_=_((abs_f1)_(#)_||.f2.||)_._c let c be Element of C; ::_thesis: ( c in dom ||.(f1 (#) f2).|| implies ||.(f1 (#) f2).|| . c = ((abs f1) (#) ||.f2.||) . c ) assume A2: c in dom ||.(f1 (#) f2).|| ; ::_thesis: ||.(f1 (#) f2).|| . c = ((abs f1) (#) ||.f2.||) . c then A3: c in dom (f1 (#) f2) by NORMSP_0:def_3; c in (dom (abs f1)) /\ (dom ||.f2.||) by A1, A2, VALUED_1:def_4; then A4: c in dom ||.f2.|| by XBOOLE_0:def_4; thus ||.(f1 (#) f2).|| . c = ||.((f1 (#) f2) /. c).|| by A2, NORMSP_0:def_3 .= ||.((f1 . c) * (f2 /. c)).|| by A3, Def3 .= (abs (f1 . c)) * ||.(f2 /. c).|| by NORMSP_1:def_1 .= ((abs f1) . c) * ||.(f2 /. c).|| by VALUED_1:18 .= ((abs f1) . c) * (||.f2.|| . c) by A4, NORMSP_0:def_3 .= ((abs f1) (#) ||.f2.||) . c by VALUED_1:5 ; ::_thesis: verum end; hence ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.|| by A1, PARTFUN1:5; ::_thesis: verum end; theorem :: VFUNCT_1:22 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.|| proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.|| let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.|| let f be PartFunc of C,V; ::_thesis: for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.|| let r be Real; ::_thesis: ||.(r (#) f).|| = (abs r) (#) ||.f.|| A1: dom ||.(r (#) f).|| = dom (r (#) f) by NORMSP_0:def_3 .= dom f by Def4 .= dom ||.f.|| by NORMSP_0:def_3 .= dom ((abs r) (#) ||.f.||) by VALUED_1:def_5 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_||.(r_(#)_f).||_holds_ ||.(r_(#)_f).||_._c_=_((abs_r)_(#)_||.f.||)_._c let c be Element of C; ::_thesis: ( c in dom ||.(r (#) f).|| implies ||.(r (#) f).|| . c = ((abs r) (#) ||.f.||) . c ) assume A2: c in dom ||.(r (#) f).|| ; ::_thesis: ||.(r (#) f).|| . c = ((abs r) (#) ||.f.||) . c then A3: c in dom ||.f.|| by A1, VALUED_1:def_5; A4: c in dom (r (#) f) by A2, NORMSP_0:def_3; thus ||.(r (#) f).|| . c = ||.((r (#) f) /. c).|| by A2, NORMSP_0:def_3 .= ||.(r * (f /. c)).|| by A4, Def4 .= (abs r) * ||.(f /. c).|| by NORMSP_1:def_1 .= (abs r) * (||.f.|| . c) by A3, NORMSP_0:def_3 .= ((abs r) (#) ||.f.||) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum end; hence ||.(r (#) f).|| = (abs r) (#) ||.f.|| by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th23: :: VFUNCT_1:23 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds - f = (- 1) (#) f proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds - f = (- 1) (#) f let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds - f = (- 1) (#) f let f be PartFunc of C,V; ::_thesis: - f = (- 1) (#) f A1: dom (- f) = dom f by Def5 .= dom ((- 1) (#) f) by Def4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((-_1)_(#)_f)_holds_ (-_f)_/._c_=_((-_1)_(#)_f)_/._c let c be Element of C; ::_thesis: ( c in dom ((- 1) (#) f) implies (- f) /. c = ((- 1) (#) f) /. c ) assume A2: c in dom ((- 1) (#) f) ; ::_thesis: (- f) /. c = ((- 1) (#) f) /. c hence (- f) /. c = - (f /. c) by A1, Def5 .= (- 1) * (f /. c) by RLVECT_1:16 .= ((- 1) (#) f) /. c by A2, Def4 ; ::_thesis: verum end; hence - f = (- 1) (#) f by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th24: :: VFUNCT_1:24 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds - (- f) = f proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds - (- f) = f let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds - (- f) = f let f be PartFunc of C,V; ::_thesis: - (- f) = f thus - (- f) = (- 1) (#) (- f) by Th23 .= (- 1) (#) ((- 1) (#) f) by Th23 .= ((- 1) * (- 1)) (#) f by Th14 .= f by Th18 ; ::_thesis: verum end; theorem Th25: :: VFUNCT_1:25 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2) let f1, f2 be PartFunc of C,V; ::_thesis: f1 - f2 = f1 + (- f2) A1: dom (f1 - f2) = (dom f1) /\ (dom f2) by Def2 .= (dom f1) /\ (dom (- f2)) by Def5 .= dom (f1 + (- f2)) by Def1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_(-_f2))_holds_ (f1_+_(-_f2))_/._c_=_(f1_-_f2)_/._c let c be Element of C; ::_thesis: ( c in dom (f1 + (- f2)) implies (f1 + (- f2)) /. c = (f1 - f2) /. c ) assume A2: c in dom (f1 + (- f2)) ; ::_thesis: (f1 + (- f2)) /. c = (f1 - f2) /. c then c in (dom f1) /\ (dom (- f2)) by Def1; then A3: c in dom (- f2) by XBOOLE_0:def_4; thus (f1 + (- f2)) /. c = (f1 /. c) + ((- f2) /. c) by A2, Def1 .= (f1 /. c) - (f2 /. c) by A3, Def5 .= (f1 - f2) /. c by A1, A2, Def2 ; ::_thesis: verum end; hence f1 - f2 = f1 + (- f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:26 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2 proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2 let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2 let f1, f2 be PartFunc of C,V; ::_thesis: f1 - (- f2) = f1 + f2 thus f1 - (- f2) = f1 + (- (- f2)) by Th25 .= f1 + f2 by Th24 ; ::_thesis: verum end; theorem Th27: :: VFUNCT_1:27 for X being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) proof let X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) let f1, f2 be PartFunc of C,V; ::_thesis: ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_(f2_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = ((f1 | X) + (f2 | X)) /. c ) assume A2: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = ((f1 | X) + (f2 | X)) /. c then A3: c in (dom (f1 + f2)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; A5: c in dom (f1 + f2) by A3, XBOOLE_0:def_4; then A6: c in (dom f1) /\ (dom f2) by Def1; then c in dom f2 by XBOOLE_0:def_4; then c in (dom f2) /\ X by A4, XBOOLE_0:def_4; then A7: c in dom (f2 | X) by RELAT_1:61; c in dom f1 by A6, XBOOLE_0:def_4; then c in (dom f1) /\ X by A4, XBOOLE_0:def_4; then A8: c in dom (f1 | X) by RELAT_1:61; then c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4; then A9: c in dom ((f1 | X) + (f2 | X)) by Def1; thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A2, PARTFUN2:15 .= (f1 /. c) + (f2 /. c) by A5, Def1 .= ((f1 | X) /. c) + (f2 /. c) by A8, PARTFUN2:15 .= ((f1 | X) /. c) + ((f2 | X) /. c) by A7, PARTFUN2:15 .= ((f1 | X) + (f2 | X)) /. c by A9, Def1 ; ::_thesis: verum end; dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ (X /\ X) by Def1 .= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16 .= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61 .= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61 .= dom ((f1 | X) + (f2 | X)) by Def1 ; hence (f1 + f2) | X = (f1 | X) + (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_f2)_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = ((f1 | X) + f2) /. c ) assume A11: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = ((f1 | X) + f2) /. c then A12: c in (dom (f1 + f2)) /\ X by RELAT_1:61; then A13: c in X by XBOOLE_0:def_4; A14: c in dom (f1 + f2) by A12, XBOOLE_0:def_4; then A15: c in (dom f1) /\ (dom f2) by Def1; then c in dom f1 by XBOOLE_0:def_4; then c in (dom f1) /\ X by A13, XBOOLE_0:def_4; then A16: c in dom (f1 | X) by RELAT_1:61; c in dom f2 by A15, XBOOLE_0:def_4; then c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4; then A17: c in dom ((f1 | X) + f2) by Def1; thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A11, PARTFUN2:15 .= (f1 /. c) + (f2 /. c) by A14, Def1 .= ((f1 | X) /. c) + (f2 /. c) by A16, PARTFUN2:15 .= ((f1 | X) + f2) /. c by A17, Def1 ; ::_thesis: verum end; dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by Def1 .= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61 .= dom ((f1 | X) + f2) by Def1 ; hence (f1 + f2) | X = (f1 | X) + f2 by A10, PARTFUN2:1; ::_thesis: (f1 + f2) | X = f1 + (f2 | X) A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_/._c_=_(f1_+_(f2_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = (f1 + (f2 | X)) /. c ) assume A19: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = (f1 + (f2 | X)) /. c then A20: c in (dom (f1 + f2)) /\ X by RELAT_1:61; then A21: c in X by XBOOLE_0:def_4; A22: c in dom (f1 + f2) by A20, XBOOLE_0:def_4; then A23: c in (dom f1) /\ (dom f2) by Def1; then c in dom f2 by XBOOLE_0:def_4; then c in (dom f2) /\ X by A21, XBOOLE_0:def_4; then A24: c in dom (f2 | X) by RELAT_1:61; c in dom f1 by A23, XBOOLE_0:def_4; then c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4; then A25: c in dom (f1 + (f2 | X)) by Def1; thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A19, PARTFUN2:15 .= (f1 /. c) + (f2 /. c) by A22, Def1 .= (f1 /. c) + ((f2 | X) /. c) by A24, PARTFUN2:15 .= (f1 + (f2 | X)) /. c by A25, Def1 ; ::_thesis: verum end; dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by Def1 .= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61 .= dom (f1 + (f2 | X)) by Def1 ; hence (f1 + f2) | X = f1 + (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:28 for X being set for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) proof let X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let f1 be PartFunc of C,REAL; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_(f2_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c ) assume A2: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c then A3: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; A5: c in dom (f1 (#) f2) by A3, XBOOLE_0:def_4; then A6: c in (dom f1) /\ (dom f2) by Def3; then c in dom f2 by XBOOLE_0:def_4; then c in (dom f2) /\ X by A4, XBOOLE_0:def_4; then A7: c in dom (f2 | X) by RELAT_1:61; c in dom f1 by A6, XBOOLE_0:def_4; then c in (dom f1) /\ X by A4, XBOOLE_0:def_4; then A8: c in dom (f1 | X) by RELAT_1:61; then c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4; then A9: c in dom ((f1 | X) (#) (f2 | X)) by Def3; thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A2, PARTFUN2:15 .= (f1 . c) * (f2 /. c) by A5, Def3 .= ((f1 | X) . c) * (f2 /. c) by A8, FUNCT_1:47 .= ((f1 | X) . c) * ((f2 | X) /. c) by A7, PARTFUN2:15 .= ((f1 | X) (#) (f2 | X)) /. c by A9, Def3 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ (X /\ X) by Def3 .= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16 .= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61 .= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61 .= dom ((f1 | X) (#) (f2 | X)) by Def3 ; hence (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_f2)_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c ) assume A11: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c then A12: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61; then A13: c in X by XBOOLE_0:def_4; A14: c in dom (f1 (#) f2) by A12, XBOOLE_0:def_4; then A15: c in (dom f1) /\ (dom f2) by Def3; then c in dom f1 by XBOOLE_0:def_4; then c in (dom f1) /\ X by A13, XBOOLE_0:def_4; then A16: c in dom (f1 | X) by RELAT_1:61; c in dom f2 by A15, XBOOLE_0:def_4; then c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4; then A17: c in dom ((f1 | X) (#) f2) by Def3; thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A11, PARTFUN2:15 .= (f1 . c) * (f2 /. c) by A14, Def3 .= ((f1 | X) . c) * (f2 /. c) by A16, FUNCT_1:47 .= ((f1 | X) (#) f2) /. c by A17, Def3 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by Def3 .= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61 .= dom ((f1 | X) (#) f2) by Def3 ; hence (f1 (#) f2) | X = (f1 | X) (#) f2 by A10, PARTFUN2:1; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X) A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_/._c_=_(f1_(#)_(f2_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c ) assume A19: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c then A20: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61; then A21: c in X by XBOOLE_0:def_4; A22: c in dom (f1 (#) f2) by A20, XBOOLE_0:def_4; then A23: c in (dom f1) /\ (dom f2) by Def3; then c in dom f2 by XBOOLE_0:def_4; then c in (dom f2) /\ X by A21, XBOOLE_0:def_4; then A24: c in dom (f2 | X) by RELAT_1:61; c in dom f1 by A23, XBOOLE_0:def_4; then c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4; then A25: c in dom (f1 (#) (f2 | X)) by Def3; thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A19, PARTFUN2:15 .= (f1 . c) * (f2 /. c) by A22, Def3 .= (f1 . c) * ((f2 | X) /. c) by A24, PARTFUN2:15 .= (f1 (#) (f2 | X)) /. c by A25, Def3 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by Def3 .= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61 .= dom (f1 (#) (f2 | X)) by Def3 ; hence (f1 (#) f2) | X = f1 (#) (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum end; theorem Th29: :: VFUNCT_1:29 for X being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| ) proof let X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| ) let f be PartFunc of C,V; ::_thesis: ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| ) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((-_f)_|_X)_holds_ ((-_f)_|_X)_/._c_=_(-_(f_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((- f) | X) implies ((- f) | X) /. c = (- (f | X)) /. c ) assume A2: c in dom ((- f) | X) ; ::_thesis: ((- f) | X) /. c = (- (f | X)) /. c then A3: c in (dom (- f)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; A5: c in dom (- f) by A3, XBOOLE_0:def_4; then c in dom f by Def5; then c in (dom f) /\ X by A4, XBOOLE_0:def_4; then A6: c in dom (f | X) by RELAT_1:61; then A7: c in dom (- (f | X)) by Def5; thus ((- f) | X) /. c = (- f) /. c by A2, PARTFUN2:15 .= - (f /. c) by A5, Def5 .= - ((f | X) /. c) by A6, PARTFUN2:15 .= (- (f | X)) /. c by A7, Def5 ; ::_thesis: verum end; dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61 .= (dom f) /\ X by Def5 .= dom (f | X) by RELAT_1:61 .= dom (- (f | X)) by Def5 ; hence (- f) | X = - (f | X) by A1, PARTFUN2:1; ::_thesis: ||.f.|| | X = ||.(f | X).|| A8: dom (||.f.|| | X) = (dom ||.f.||) /\ X by RELAT_1:61 .= (dom f) /\ X by NORMSP_0:def_3 .= dom (f | X) by RELAT_1:61 .= dom ||.(f | X).|| by NORMSP_0:def_3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(||.f.||_|_X)_holds_ (||.f.||_|_X)_._c_=_||.(f_|_X).||_._c let c be Element of C; ::_thesis: ( c in dom (||.f.|| | X) implies (||.f.|| | X) . c = ||.(f | X).|| . c ) assume A9: c in dom (||.f.|| | X) ; ::_thesis: (||.f.|| | X) . c = ||.(f | X).|| . c then A10: c in dom (f | X) by A8, NORMSP_0:def_3; c in (dom ||.f.||) /\ X by A9, RELAT_1:61; then A11: c in dom ||.f.|| by XBOOLE_0:def_4; thus (||.f.|| | X) . c = ||.f.|| . c by A9, FUNCT_1:47 .= ||.(f /. c).|| by A11, NORMSP_0:def_3 .= ||.((f | X) /. c).|| by A10, PARTFUN2:15 .= ||.(f | X).|| . c by A8, A9, NORMSP_0:def_3 ; ::_thesis: verum end; hence ||.f.|| | X = ||.(f | X).|| by A8, PARTFUN1:5; ::_thesis: verum end; theorem :: VFUNCT_1:30 for X being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) proof let X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) let f1, f2 be PartFunc of C,V; ::_thesis: ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) thus (f1 - f2) | X = (f1 + (- f2)) | X by Th25 .= (f1 | X) + ((- f2) | X) by Th27 .= (f1 | X) + (- (f2 | X)) by Th29 .= (f1 | X) - (f2 | X) by Th25 ; ::_thesis: ( (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) thus (f1 - f2) | X = (f1 + (- f2)) | X by Th25 .= (f1 | X) + (- f2) by Th27 .= (f1 | X) - f2 by Th25 ; ::_thesis: (f1 - f2) | X = f1 - (f2 | X) thus (f1 - f2) | X = (f1 + (- f2)) | X by Th25 .= f1 + ((- f2) | X) by Th27 .= f1 + (- (f2 | X)) by Th29 .= f1 - (f2 | X) by Th25 ; ::_thesis: verum end; theorem :: VFUNCT_1:31 for X being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real holds (r (#) f) | X = r (#) (f | X) proof let X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real holds (r (#) f) | X = r (#) (f | X) let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r being Real holds (r (#) f) | X = r (#) (f | X) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r being Real holds (r (#) f) | X = r (#) (f | X) let f be PartFunc of C,V; ::_thesis: for r being Real holds (r (#) f) | X = r (#) (f | X) let r be Real; ::_thesis: (r (#) f) | X = r (#) (f | X) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_(#)_f)_|_X)_holds_ ((r_(#)_f)_|_X)_/._c_=_(r_(#)_(f_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((r (#) f) | X) implies ((r (#) f) | X) /. c = (r (#) (f | X)) /. c ) assume A2: c in dom ((r (#) f) | X) ; ::_thesis: ((r (#) f) | X) /. c = (r (#) (f | X)) /. c then A3: c in (dom (r (#) f)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; A5: c in dom (r (#) f) by A3, XBOOLE_0:def_4; then c in dom f by Def4; then c in (dom f) /\ X by A4, XBOOLE_0:def_4; then A6: c in dom (f | X) by RELAT_1:61; then A7: c in dom (r (#) (f | X)) by Def4; thus ((r (#) f) | X) /. c = (r (#) f) /. c by A2, PARTFUN2:15 .= r * (f /. c) by A5, Def4 .= r * ((f | X) /. c) by A6, PARTFUN2:15 .= (r (#) (f | X)) /. c by A7, Def4 ; ::_thesis: verum end; dom ((r (#) f) | X) = (dom (r (#) f)) /\ X by RELAT_1:61 .= (dom f) /\ X by Def4 .= dom (f | X) by RELAT_1:61 .= dom (r (#) (f | X)) by Def4 ; hence (r (#) f) | X = r (#) (f | X) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: VFUNCT_1:32 for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) ) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) ) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V holds ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) ) let f1, f2 be PartFunc of C,V; ::_thesis: ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) ) thus ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) ::_thesis: ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) proof thus ( f1 is total & f2 is total implies f1 + f2 is total ) ; ::_thesis: ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) assume f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 + f2) = C by PARTFUN1:def_2; then (dom f1) /\ (dom f2) = C by Def1; then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; thus ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) ::_thesis: verum proof thus ( f1 is total & f2 is total implies f1 - f2 is total ) ; ::_thesis: ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) assume f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 - f2) = C by PARTFUN1:def_2; then (dom f1) /\ (dom f2) = C by Def2; then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; theorem :: VFUNCT_1:33 for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total ) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total ) let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL holds ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total ) let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL holds ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total ) let f1 be PartFunc of C,REAL; ::_thesis: ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total ) thus ( f1 is total & f2 is total implies f1 (#) f2 is total ) ; ::_thesis: ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) assume f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 (#) f2) = C by PARTFUN1:def_2; then (dom f1) /\ (dom f2) = C by Def3; then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th34: :: VFUNCT_1:34 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real holds ( f is total iff r (#) f is total ) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r being Real holds ( f is total iff r (#) f is total ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r being Real holds ( f is total iff r (#) f is total ) let f be PartFunc of C,V; ::_thesis: for r being Real holds ( f is total iff r (#) f is total ) let r be Real; ::_thesis: ( f is total iff r (#) f is total ) thus ( f is total implies r (#) f is total ) ; ::_thesis: ( r (#) f is total implies f is total ) assume r (#) f is total ; ::_thesis: f is total then dom (r (#) f) = C by PARTFUN1:def_2; hence dom f = C by Def4; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem :: VFUNCT_1:35 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds ( f is total iff - f is total ) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds ( f is total iff - f is total ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds ( f is total iff - f is total ) let f be PartFunc of C,V; ::_thesis: ( f is total iff - f is total ) thus ( f is total implies - f is total ) ; ::_thesis: ( - f is total implies f is total ) assume A1: - f is total ; ::_thesis: f is total - f = (- 1) (#) f by Th23; hence f is total by A1, Th34; ::_thesis: verum end; theorem Th36: :: VFUNCT_1:36 for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds ( f is total iff ||.f.|| is total ) proof let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds ( f is total iff ||.f.|| is total ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds ( f is total iff ||.f.|| is total ) let f be PartFunc of C,V; ::_thesis: ( f is total iff ||.f.|| is total ) thus ( f is total implies ||.f.|| is total ) ::_thesis: ( ||.f.|| is total implies f is total ) proof assume f is total ; ::_thesis: ||.f.|| is total then dom f = C by PARTFUN1:def_2; hence dom ||.f.|| = C by NORMSP_0:def_3; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume ||.f.|| is total ; ::_thesis: f is total then dom ||.f.|| = C by PARTFUN1:def_2; hence dom f = C by NORMSP_0:def_3; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem :: VFUNCT_1:37 for C being non empty set for c being Element of C for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) proof let C be non empty set ; ::_thesis: for c being Element of C for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) let c be Element of C; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is total & f2 is total implies ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) ) assume A1: ( f1 is total & f2 is total ) ; ::_thesis: ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) then dom (f1 + f2) = C by PARTFUN1:def_2; hence (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by Def1; ::_thesis: (f1 - f2) /. c = (f1 /. c) - (f2 /. c) dom (f1 - f2) = C by A1, PARTFUN1:def_2; hence (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by Def2; ::_thesis: verum end; theorem :: VFUNCT_1:38 for C being non empty set for c being Element of C for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) proof let C be non empty set ; ::_thesis: for c being Element of C for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) let c be Element of C; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) let f1 be PartFunc of C,REAL; ::_thesis: ( f1 is total & f2 is total implies (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) ) assume ( f1 is total & f2 is total ) ; ::_thesis: (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) then dom (f1 (#) f2) = C by PARTFUN1:def_2; hence (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) by Def3; ::_thesis: verum end; theorem :: VFUNCT_1:39 for C being non empty set for c being Element of C for V being RealNormSpace for f being PartFunc of C,V for r being Real st f is total holds (r (#) f) /. c = r * (f /. c) proof let C be non empty set ; ::_thesis: for c being Element of C for V being RealNormSpace for f being PartFunc of C,V for r being Real st f is total holds (r (#) f) /. c = r * (f /. c) let c be Element of C; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r being Real st f is total holds (r (#) f) /. c = r * (f /. c) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r being Real st f is total holds (r (#) f) /. c = r * (f /. c) let f be PartFunc of C,V; ::_thesis: for r being Real st f is total holds (r (#) f) /. c = r * (f /. c) let r be Real; ::_thesis: ( f is total implies (r (#) f) /. c = r * (f /. c) ) assume f is total ; ::_thesis: (r (#) f) /. c = r * (f /. c) then dom (r (#) f) = C by PARTFUN1:def_2; hence (r (#) f) /. c = r * (f /. c) by Def4; ::_thesis: verum end; theorem :: VFUNCT_1:40 for C being non empty set for c being Element of C for V being RealNormSpace for f being PartFunc of C,V st f is total holds ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) proof let C be non empty set ; ::_thesis: for c being Element of C for V being RealNormSpace for f being PartFunc of C,V st f is total holds ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) let c be Element of C; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st f is total holds ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f is total holds ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) let f be PartFunc of C,V; ::_thesis: ( f is total implies ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) ) assume A1: f is total ; ::_thesis: ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) then dom (- f) = C by PARTFUN1:def_2; hence (- f) /. c = - (f /. c) by Def5; ::_thesis: ||.f.|| . c = ||.(f /. c).|| ||.f.|| is total by A1, Th36; then dom ||.f.|| = C by PARTFUN1:def_2; hence ||.f.|| . c = ||.(f /. c).|| by NORMSP_0:def_3; ::_thesis: verum end; definition let C be non empty set ; let V be non empty NORMSTR ; let f be PartFunc of C,V; let Y be set ; predf is_bounded_on Y means :Def6: :: VFUNCT_1:def 6 ex r being Real st for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= r; end; :: deftheorem Def6 defines is_bounded_on VFUNCT_1:def_6_:_ for C being non empty set for V being non empty NORMSTR for f being PartFunc of C,V for Y being set holds ( f is_bounded_on Y iff ex r being Real st for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= r ); theorem :: VFUNCT_1:41 for Y, X being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds f is_bounded_on Y proof let Y, X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds f is_bounded_on Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds f is_bounded_on Y let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds f is_bounded_on Y let f be PartFunc of C,V; ::_thesis: ( Y c= X & f is_bounded_on X implies f is_bounded_on Y ) assume that A1: Y c= X and A2: f is_bounded_on X ; ::_thesis: f is_bounded_on Y consider r being Real such that A3: for c being Element of C st c in X /\ (dom f) holds ||.(f /. c).|| <= r by A2, Def6; take r ; :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= r let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies ||.(f /. c).|| <= r ) assume c in Y /\ (dom f) ; ::_thesis: ||.(f /. c).|| <= r then ( c in Y & c in dom f ) by XBOOLE_0:def_4; then c in X /\ (dom f) by A1, XBOOLE_0:def_4; hence ||.(f /. c).|| <= r by A3; ::_thesis: verum end; theorem :: VFUNCT_1:42 for X being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st X misses dom f holds f is_bounded_on X proof let X be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st X misses dom f holds f is_bounded_on X let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st X misses dom f holds f is_bounded_on X let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st X misses dom f holds f is_bounded_on X let f be PartFunc of C,V; ::_thesis: ( X misses dom f implies f is_bounded_on X ) assume X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f is_bounded_on X then for c being Element of C st c in X /\ (dom f) holds ||.(f /. c).|| <= 0 ; hence f is_bounded_on X by Def6; ::_thesis: verum end; theorem :: VFUNCT_1:43 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y let f be PartFunc of C,V; ::_thesis: 0 (#) f is_bounded_on Y now__::_thesis:_ex_p_being_Element_of_NAT_st_ for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(0_(#)_f))_holds_ ||.((0_(#)_f)_/._c).||_<=_p take p = 0 ; ::_thesis: for c being Element of C st c in Y /\ (dom (0 (#) f)) holds ||.((0 (#) f) /. c).|| <= p let c be Element of C; ::_thesis: ( c in Y /\ (dom (0 (#) f)) implies ||.((0 (#) f) /. c).|| <= p ) 0 * ||.(f /. c).|| = 0 ; then (abs 0) * ||.(f /. c).|| <= 0 by ABSVALUE:2; then A1: ||.(0 * (f /. c)).|| <= 0 by NORMSP_1:def_1; assume c in Y /\ (dom (0 (#) f)) ; ::_thesis: ||.((0 (#) f) /. c).|| <= p then c in dom (0 (#) f) by XBOOLE_0:def_4; hence ||.((0 (#) f) /. c).|| <= p by A1, Def4; ::_thesis: verum end; hence 0 (#) f is_bounded_on Y by Def6; ::_thesis: verum end; theorem Th44: :: VFUNCT_1:44 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real st f is_bounded_on Y holds r (#) f is_bounded_on Y proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for r being Real st f is_bounded_on Y holds r (#) f is_bounded_on Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for r being Real st f is_bounded_on Y holds r (#) f is_bounded_on Y let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for r being Real st f is_bounded_on Y holds r (#) f is_bounded_on Y let f be PartFunc of C,V; ::_thesis: for r being Real st f is_bounded_on Y holds r (#) f is_bounded_on Y let r be Real; ::_thesis: ( f is_bounded_on Y implies r (#) f is_bounded_on Y ) assume f is_bounded_on Y ; ::_thesis: r (#) f is_bounded_on Y then consider r1 being Real such that A1: for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= r1 by Def6; take p = (abs r) * (abs r1); :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in Y /\ (dom (r (#) f)) holds ||.((r (#) f) /. c).|| <= p let c be Element of C; ::_thesis: ( c in Y /\ (dom (r (#) f)) implies ||.((r (#) f) /. c).|| <= p ) assume A2: c in Y /\ (dom (r (#) f)) ; ::_thesis: ||.((r (#) f) /. c).|| <= p then A3: c in Y by XBOOLE_0:def_4; A4: c in dom (r (#) f) by A2, XBOOLE_0:def_4; then c in dom f by Def4; then c in Y /\ (dom f) by A3, XBOOLE_0:def_4; then A5: ||.(f /. c).|| <= r1 by A1; r1 <= abs r1 by ABSVALUE:4; then ( abs r >= 0 & ||.(f /. c).|| <= abs r1 ) by A5, COMPLEX1:46, XXREAL_0:2; then (abs r) * ||.(f /. c).|| <= (abs r) * (abs r1) by XREAL_1:64; then ||.(r * (f /. c)).|| <= p by NORMSP_1:def_1; hence ||.((r (#) f) /. c).|| <= p by A4, Def4; ::_thesis: verum end; theorem Th45: :: VFUNCT_1:45 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f is_bounded_on Y holds ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f is_bounded_on Y holds ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st f is_bounded_on Y holds ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f is_bounded_on Y holds ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) let f be PartFunc of C,V; ::_thesis: ( f is_bounded_on Y implies ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) ) assume A1: f is_bounded_on Y ; ::_thesis: ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) then consider r1 being Real such that A2: for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= r1 by Def6; now__::_thesis:_for_c_being_set_st_c_in_Y_/\_(dom_||.f.||)_holds_ abs_(||.f.||_._c)_<=_r1 let c be set ; ::_thesis: ( c in Y /\ (dom ||.f.||) implies abs (||.f.|| . c) <= r1 ) assume A3: c in Y /\ (dom ||.f.||) ; ::_thesis: abs (||.f.|| . c) <= r1 then A4: c in Y by XBOOLE_0:def_4; A5: c in dom ||.f.|| by A3, XBOOLE_0:def_4; then c in dom f by NORMSP_0:def_3; then c in Y /\ (dom f) by A4, XBOOLE_0:def_4; then ( ||.(f /. c).|| >= 0 & ||.(f /. c).|| <= r1 ) by A2, NORMSP_1:4; then abs ||.(f /. c).|| <= r1 by ABSVALUE:def_1; hence abs (||.f.|| . c) <= r1 by A5, NORMSP_0:def_3; ::_thesis: verum end; hence ||.f.|| | Y is bounded by RFUNCT_1:73; ::_thesis: - f is_bounded_on Y (- 1) (#) f is_bounded_on Y by A1, Th44; hence - f is_bounded_on Y by Th23; ::_thesis: verum end; theorem Th46: :: VFUNCT_1:46 for X, Y being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 + f2 is_bounded_on X /\ Y proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 + f2 is_bounded_on X /\ Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 + f2 is_bounded_on X /\ Y let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 + f2 is_bounded_on X /\ Y let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 is_bounded_on Y implies f1 + f2 is_bounded_on X /\ Y ) assume that A1: f1 is_bounded_on X and A2: f2 is_bounded_on Y ; ::_thesis: f1 + f2 is_bounded_on X /\ Y consider r1 being Real such that A3: for c being Element of C st c in X /\ (dom f1) holds ||.(f1 /. c).|| <= r1 by A1, Def6; consider r2 being Real such that A4: for c being Element of C st c in Y /\ (dom f2) holds ||.(f2 /. c).|| <= r2 by A2, Def6; take r = r1 + r2; :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds ||.((f1 + f2) /. c).|| <= r let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies ||.((f1 + f2) /. c).|| <= r ) assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: ||.((f1 + f2) /. c).|| <= r then A6: c in X /\ Y by XBOOLE_0:def_4; then A7: c in Y by XBOOLE_0:def_4; A8: c in dom (f1 + f2) by A5, XBOOLE_0:def_4; then A9: c in (dom f1) /\ (dom f2) by Def1; then c in dom f2 by XBOOLE_0:def_4; then c in Y /\ (dom f2) by A7, XBOOLE_0:def_4; then A10: ||.(f2 /. c).|| <= r2 by A4; A11: c in X by A6, XBOOLE_0:def_4; c in dom f1 by A9, XBOOLE_0:def_4; then c in X /\ (dom f1) by A11, XBOOLE_0:def_4; then ||.(f1 /. c).|| <= r1 by A3; then ( ||.((f1 /. c) + (f2 /. c)).|| <= ||.(f1 /. c).|| + ||.(f2 /. c).|| & ||.(f1 /. c).|| + ||.(f2 /. c).|| <= r ) by A10, NORMSP_1:def_1, XREAL_1:7; then ||.((f1 /. c) + (f2 /. c)).|| <= r by XXREAL_0:2; hence ||.((f1 + f2) /. c).|| <= r by A8, Def1; ::_thesis: verum end; theorem :: VFUNCT_1:47 for X, Y being set for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds f1 (#) f2 is_bounded_on X /\ Y proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds f1 (#) f2 is_bounded_on X /\ Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds f1 (#) f2 is_bounded_on X /\ Y let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds f1 (#) f2 is_bounded_on X /\ Y let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds f1 (#) f2 is_bounded_on X /\ Y let f1 be PartFunc of C,REAL; ::_thesis: ( f1 | X is bounded & f2 is_bounded_on Y implies f1 (#) f2 is_bounded_on X /\ Y ) assume that A1: f1 | X is bounded and A2: f2 is_bounded_on Y ; ::_thesis: f1 (#) f2 is_bounded_on X /\ Y consider r1 being real number such that A3: for c being set st c in X /\ (dom f1) holds abs (f1 . c) <= r1 by A1, RFUNCT_1:73; consider r2 being Real such that A4: for c being Element of C st c in Y /\ (dom f2) holds ||.(f2 /. c).|| <= r2 by A2, Def6; reconsider r1 = r1 as Real by XREAL_0:def_1; now__::_thesis:_ex_r_being_Element_of_REAL_st_ for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_ ||.((f1_(#)_f2)_/._c).||_<=_r take r = r1 * r2; ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds ||.((f1 (#) f2) /. c).|| <= r let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies ||.((f1 (#) f2) /. c).|| <= r ) assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: ||.((f1 (#) f2) /. c).|| <= r then A6: c in X /\ Y by XBOOLE_0:def_4; then A7: c in X by XBOOLE_0:def_4; A8: c in dom (f1 (#) f2) by A5, XBOOLE_0:def_4; then A9: c in (dom f1) /\ (dom f2) by Def3; then c in dom f1 by XBOOLE_0:def_4; then c in X /\ (dom f1) by A7, XBOOLE_0:def_4; then A10: abs (f1 . c) <= r1 by A3; A11: c in Y by A6, XBOOLE_0:def_4; c in dom f2 by A9, XBOOLE_0:def_4; then c in Y /\ (dom f2) by A11, XBOOLE_0:def_4; then A12: ||.(f2 /. c).|| <= r2 by A4; ( 0 <= abs (f1 . c) & 0 <= ||.(f2 /. c).|| ) by COMPLEX1:46, NORMSP_1:4; then (abs (f1 . c)) * ||.(f2 /. c).|| <= r by A10, A12, XREAL_1:66; then ||.((f1 . c) * (f2 /. c)).|| <= r by NORMSP_1:def_1; hence ||.((f1 (#) f2) /. c).|| <= r by A8, Def3; ::_thesis: verum end; hence f1 (#) f2 is_bounded_on X /\ Y by Def6; ::_thesis: verum end; theorem :: VFUNCT_1:48 for X, Y being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 - f2 is_bounded_on X /\ Y proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 - f2 is_bounded_on X /\ Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 - f2 is_bounded_on X /\ Y let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds f1 - f2 is_bounded_on X /\ Y let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 is_bounded_on Y implies f1 - f2 is_bounded_on X /\ Y ) assume that A1: f1 is_bounded_on X and A2: f2 is_bounded_on Y ; ::_thesis: f1 - f2 is_bounded_on X /\ Y - f2 is_bounded_on Y by A2, Th45; then f1 + (- f2) is_bounded_on X /\ Y by A1, Th46; hence f1 - f2 is_bounded_on X /\ Y by Th25; ::_thesis: verum end; theorem :: VFUNCT_1:49 for X, Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds f is_bounded_on X \/ Y proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds f is_bounded_on X \/ Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds f is_bounded_on X \/ Y let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds f is_bounded_on X \/ Y let f be PartFunc of C,V; ::_thesis: ( f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y ) assume that A1: f is_bounded_on X and A2: f is_bounded_on Y ; ::_thesis: f is_bounded_on X \/ Y consider r1 being Real such that A3: for c being Element of C st c in X /\ (dom f) holds ||.(f /. c).|| <= r1 by A1, Def6; consider r2 being Real such that A4: for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= r2 by A2, Def6; take r = (abs r1) + (abs r2); :: according to VFUNCT_1:def_6 ::_thesis: for c being Element of C st c in (X \/ Y) /\ (dom f) holds ||.(f /. c).|| <= r let c be Element of C; ::_thesis: ( c in (X \/ Y) /\ (dom f) implies ||.(f /. c).|| <= r ) assume A5: c in (X \/ Y) /\ (dom f) ; ::_thesis: ||.(f /. c).|| <= r then A6: c in dom f by XBOOLE_0:def_4; A7: c in X \/ Y by A5, XBOOLE_0:def_4; now__::_thesis:_||.(f_/._c).||_<=_r percases ( c in X or c in Y ) by A7, XBOOLE_0:def_3; suppose c in X ; ::_thesis: ||.(f /. c).|| <= r then c in X /\ (dom f) by A6, XBOOLE_0:def_4; then A8: ||.(f /. c).|| <= r1 by A3; A9: 0 <= abs r2 by COMPLEX1:46; r1 <= abs r1 by ABSVALUE:4; then ||.(f /. c).|| <= abs r1 by A8, XXREAL_0:2; then ||.(f /. c).|| + 0 <= r by A9, XREAL_1:7; hence ||.(f /. c).|| <= r ; ::_thesis: verum end; suppose c in Y ; ::_thesis: ||.(f /. c).|| <= r then c in Y /\ (dom f) by A6, XBOOLE_0:def_4; then A10: ||.(f /. c).|| <= r2 by A4; A11: 0 <= abs r1 by COMPLEX1:46; r2 <= abs r2 by ABSVALUE:4; then ||.(f /. c).|| <= abs r2 by A10, XXREAL_0:2; then 0 + ||.(f /. c).|| <= r by A11, XREAL_1:7; hence ||.(f /. c).|| <= r ; ::_thesis: verum end; end; end; hence ||.(f /. c).|| <= r ; ::_thesis: verum end; theorem :: VFUNCT_1:50 for X, Y being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 | X is V8() & f2 | Y is V8() implies ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) ) assume that A1: f1 | X is V8() and A2: f2 | Y is V8() ; ::_thesis: ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) consider r1 being VECTOR of V such that A3: for c being Element of C st c in X /\ (dom f1) holds f1 /. c = r1 by A1, PARTFUN2:35; consider r2 being VECTOR of V such that A4: for c being Element of C st c in Y /\ (dom f2) holds f2 /. c = r2 by A2, PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_ (f1_+_f2)_/._c_=_r1_+_r2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = r1 + r2 ) assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: (f1 + f2) /. c = r1 + r2 then A6: c in X /\ Y by XBOOLE_0:def_4; then A7: c in X by XBOOLE_0:def_4; A8: c in dom (f1 + f2) by A5, XBOOLE_0:def_4; then A9: c in (dom f1) /\ (dom f2) by Def1; then c in dom f1 by XBOOLE_0:def_4; then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def_4; A11: c in Y by A6, XBOOLE_0:def_4; c in dom f2 by A9, XBOOLE_0:def_4; then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def_4; thus (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by A8, Def1 .= r1 + (f2 /. c) by A3, A10 .= r1 + r2 by A4, A12 ; ::_thesis: verum end; hence (f1 + f2) | (X /\ Y) is V8() by PARTFUN2:35; ::_thesis: (f1 - f2) | (X /\ Y) is V8() now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_-_f2))_holds_ (f1_-_f2)_/._c_=_r1_-_r2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = r1 - r2 ) assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; ::_thesis: (f1 - f2) /. c = r1 - r2 then A14: c in X /\ Y by XBOOLE_0:def_4; then A15: c in X by XBOOLE_0:def_4; A16: c in dom (f1 - f2) by A13, XBOOLE_0:def_4; then A17: c in (dom f1) /\ (dom f2) by Def2; then c in dom f1 by XBOOLE_0:def_4; then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def_4; A19: c in Y by A14, XBOOLE_0:def_4; c in dom f2 by A17, XBOOLE_0:def_4; then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def_4; thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A16, Def2 .= r1 - (f2 /. c) by A3, A18 .= r1 - r2 by A4, A20 ; ::_thesis: verum end; hence (f1 - f2) | (X /\ Y) is V8() by PARTFUN2:35; ::_thesis: verum end; theorem :: VFUNCT_1:51 for X, Y being set for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds (f1 (#) f2) | (X /\ Y) is V8() proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds (f1 (#) f2) | (X /\ Y) is V8() let C be non empty set ; ::_thesis: for V being RealNormSpace for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds (f1 (#) f2) | (X /\ Y) is V8() let V be RealNormSpace; ::_thesis: for f2 being PartFunc of C,V for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds (f1 (#) f2) | (X /\ Y) is V8() let f2 be PartFunc of C,V; ::_thesis: for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds (f1 (#) f2) | (X /\ Y) is V8() let f1 be PartFunc of C,REAL; ::_thesis: ( f1 | X is V8() & f2 | Y is V8() implies (f1 (#) f2) | (X /\ Y) is V8() ) assume that A1: f1 | X is V8() and A2: f2 | Y is V8() ; ::_thesis: (f1 (#) f2) | (X /\ Y) is V8() consider r1 being Real such that A3: for c being Element of C st c in X /\ (dom f1) holds f1 . c = r1 by A1, PARTFUN2:57; consider r2 being VECTOR of V such that A4: for c being Element of C st c in Y /\ (dom f2) holds f2 /. c = r2 by A2, PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_ (f1_(#)_f2)_/._c_=_r1_*_r2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = r1 * r2 ) assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) /. c = r1 * r2 then A6: c in X /\ Y by XBOOLE_0:def_4; then A7: c in X by XBOOLE_0:def_4; A8: c in dom (f1 (#) f2) by A5, XBOOLE_0:def_4; then A9: c in (dom f1) /\ (dom f2) by Def3; then c in dom f1 by XBOOLE_0:def_4; then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def_4; A11: c in Y by A6, XBOOLE_0:def_4; c in dom f2 by A9, XBOOLE_0:def_4; then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def_4; thus (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) by A8, Def3 .= r1 * (f2 /. c) by A3, A10 .= r1 * r2 by A4, A12 ; ::_thesis: verum end; hence (f1 (#) f2) | (X /\ Y) is V8() by PARTFUN2:35; ::_thesis: verum end; theorem Th52: :: VFUNCT_1:52 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for p being Real st f | Y is V8() holds (p (#) f) | Y is V8() proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V for p being Real st f | Y is V8() holds (p (#) f) | Y is V8() let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V for p being Real st f | Y is V8() holds (p (#) f) | Y is V8() let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V for p being Real st f | Y is V8() holds (p (#) f) | Y is V8() let f be PartFunc of C,V; ::_thesis: for p being Real st f | Y is V8() holds (p (#) f) | Y is V8() let p be Real; ::_thesis: ( f | Y is V8() implies (p (#) f) | Y is V8() ) assume f | Y is V8() ; ::_thesis: (p (#) f) | Y is V8() then consider r being VECTOR of V such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = r by PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(p_(#)_f))_holds_ (p_(#)_f)_/._c_=_p_*_r let c be Element of C; ::_thesis: ( c in Y /\ (dom (p (#) f)) implies (p (#) f) /. c = p * r ) assume A2: c in Y /\ (dom (p (#) f)) ; ::_thesis: (p (#) f) /. c = p * r then A3: c in Y by XBOOLE_0:def_4; A4: c in dom (p (#) f) by A2, XBOOLE_0:def_4; then c in dom f by Def4; then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4; thus (p (#) f) /. c = p * (f /. c) by A4, Def4 .= p * r by A1, A5 ; ::_thesis: verum end; hence (p (#) f) | Y is V8() by PARTFUN2:35; ::_thesis: verum end; theorem Th53: :: VFUNCT_1:53 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f | Y is V8() holds ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) let f be PartFunc of C,V; ::_thesis: ( f | Y is V8() implies ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) ) assume f | Y is V8() ; ::_thesis: ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) then consider r being VECTOR of V such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = r by PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_||.f.||)_holds_ ||.f.||_._c_=_||.r.|| let c be Element of C; ::_thesis: ( c in Y /\ (dom ||.f.||) implies ||.f.|| . c = ||.r.|| ) assume A2: c in Y /\ (dom ||.f.||) ; ::_thesis: ||.f.|| . c = ||.r.|| then A3: c in Y by XBOOLE_0:def_4; A4: c in dom ||.f.|| by A2, XBOOLE_0:def_4; then c in dom f by NORMSP_0:def_3; then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4; thus ||.f.|| . c = ||.(f /. c).|| by A4, NORMSP_0:def_3 .= ||.r.|| by A1, A5 ; ::_thesis: verum end; hence ||.f.|| | Y is V8() by PARTFUN2:57; ::_thesis: (- f) | Y is V8() now__::_thesis:_ex_p_being_Element_of_the_U1_of_V_st_ for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(-_f))_holds_ (-_f)_/._c_=_p take p = - r; ::_thesis: for c being Element of C st c in Y /\ (dom (- f)) holds (- f) /. c = p let c be Element of C; ::_thesis: ( c in Y /\ (dom (- f)) implies (- f) /. c = p ) assume A6: c in Y /\ (dom (- f)) ; ::_thesis: (- f) /. c = p then c in Y /\ (dom f) by Def5; then A7: - (f /. c) = p by A1; c in dom (- f) by A6, XBOOLE_0:def_4; hence (- f) /. c = p by A7, Def5; ::_thesis: verum end; hence (- f) | Y is V8() by PARTFUN2:35; ::_thesis: verum end; theorem Th54: :: VFUNCT_1:54 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds f is_bounded_on Y proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds f is_bounded_on Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds f is_bounded_on Y let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f | Y is V8() holds f is_bounded_on Y let f be PartFunc of C,V; ::_thesis: ( f | Y is V8() implies f is_bounded_on Y ) assume f | Y is V8() ; ::_thesis: f is_bounded_on Y then consider r being VECTOR of V such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = r by PARTFUN2:35; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_ ||.(f_/._c).||_<=_p take p = ||.r.||; ::_thesis: for c being Element of C st c in Y /\ (dom f) holds ||.(f /. c).|| <= p let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies ||.(f /. c).|| <= p ) assume c in Y /\ (dom f) ; ::_thesis: ||.(f /. c).|| <= p hence ||.(f /. c).|| <= p by A1; ::_thesis: verum end; hence f is_bounded_on Y by Def6; ::_thesis: verum end; theorem :: VFUNCT_1:55 for Y being set for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) proof let Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f being PartFunc of C,V st f | Y is V8() holds ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) let V be RealNormSpace; ::_thesis: for f being PartFunc of C,V st f | Y is V8() holds ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) let f be PartFunc of C,V; ::_thesis: ( f | Y is V8() implies ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) ) assume A1: f | Y is V8() ; ::_thesis: ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) hereby ::_thesis: ( - f is_bounded_on Y & ||.f.|| | Y is bounded ) let r be Real; ::_thesis: r (#) f is_bounded_on Y (r (#) f) | Y is V8() by A1, Th52; hence r (#) f is_bounded_on Y by Th54; ::_thesis: verum end; (- f) | Y is V8() by A1, Th53; hence - f is_bounded_on Y by Th54; ::_thesis: ||.f.|| | Y is bounded ||.f.|| | Y is V8() by A1, Th53; hence ||.f.|| | Y is bounded ; ::_thesis: verum end; theorem :: VFUNCT_1:56 for X, Y being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds f1 + f2 is_bounded_on X /\ Y proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds f1 + f2 is_bounded_on X /\ Y let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds f1 + f2 is_bounded_on X /\ Y let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds f1 + f2 is_bounded_on X /\ Y let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 | Y is V8() implies f1 + f2 is_bounded_on X /\ Y ) assume that A1: f1 is_bounded_on X and A2: f2 | Y is V8() ; ::_thesis: f1 + f2 is_bounded_on X /\ Y f2 is_bounded_on Y by A2, Th54; hence f1 + f2 is_bounded_on X /\ Y by A1, Th46; ::_thesis: verum end; theorem :: VFUNCT_1:57 for X, Y being set for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) proof let X, Y be set ; ::_thesis: for C being non empty set for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) let C be non empty set ; ::_thesis: for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) let V be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) let f1, f2 be PartFunc of C,V; ::_thesis: ( f1 is_bounded_on X & f2 | Y is V8() implies ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) ) assume that A1: f1 is_bounded_on X and A2: f2 | Y is V8() ; ::_thesis: ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) A3: f2 is_bounded_on Y by A2, Th54; then - f2 is_bounded_on Y by Th45; then A4: f1 + (- f2) is_bounded_on X /\ Y by A1, Th46; - f1 is_bounded_on X by A1, Th45; then f2 + (- f1) is_bounded_on Y /\ X by A3, Th46; hence ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y ) by A4, Th25; ::_thesis: verum end;