:: Algebra of Complex Vector Valued Functions :: by Noboru Endou :: :: Received August 20, 2004 :: Copyright (c) 2004-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, CLVECT_1, PARTFUN1, XCMPLX_0, SUBSET_1, ARYTM_3, ARYTM_1, RELAT_1, NUMBERS, VALUED_1, NORMSP_1, FUNCT_1, SUPINF_2, CARD_1, TARSKI, COMPLEX1, VFUNCT_1, REAL_1, XXREAL_0, XXREAL_2, RLVECT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, RLVECT_1, VALUED_1, COMSEQ_2, COMPLEX1, NORMSP_0, CLVECT_1, XXREAL_0, VFUNCT_1; constructors REAL_1, COMPLEX1, CLVECT_1, VALUED_1, RELSET_1, VFUNCT_1, COMSEQ_2; registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0, RFUNCT_1, XCMPLX_0; requirements SUBSET, BOOLE, ARITHM, NUMERALS; definitions TARSKI, PARTFUN1, XBOOLE_0; equalities XBOOLE_0, RLVECT_1, VALUED_1; expansions PARTFUN1, XBOOLE_0; theorems TARSKI, SUBSET_1, FUNCT_1, ABSVALUE, PARTFUN1, PARTFUN2, RFUNCT_1, RLVECT_1, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, CLVECT_1, COMPLEX1, CFUNCT_1, XREAL_1, XXREAL_0, VALUED_1, NORMSP_0, VFUNCT_1; schemes PARTFUN2; begin reserve M for non empty set; reserve V for ComplexNormSpace; reserve f,f1,f2,f3 for PartFunc of M,V; reserve z,z1,z2 for Complex; :: ::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF COMPLEX NUMBERS :: definition let M be non empty set; let V be ComplexNormSpace; let f1 be PartFunc of M, COMPLEX; let f2 be PartFunc of M, V; deffunc F(Element of M) = (f1/.\$1) * (f2/.\$1); defpred P[set] means \$1 in dom f1 /\ dom f2; set X = dom f1 /\ dom f2; func f1(#)f2 -> PartFunc of M,V means :Def1: dom it = dom f1 /\ dom f2 & for c be Element of M st c in dom it holds it/.c = (f1/.c) * (f2/.c); existence proof consider F be PartFunc of M,V such that A1: for c be Element of M holds c in dom F iff P[c] and A2: for c be Element of M st c in dom F holds F/.c = F(c) from PARTFUN2:sch 2; take F; thus dom F = dom f1 /\ dom f2 by A1,SUBSET_1:3; let c be Element of M; assume c in dom F; hence thesis by A2; end; uniqueness proof thus for f,g being PartFunc of M,V st (dom f=X & for c be Element of M st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of M st c in dom g holds g/.c = F(c)) holds f = g from PARTFUN2:sch 3; end; end; definition let X be non empty set; let V be ComplexNormSpace; let f be PartFunc of X,V; let z be Complex; deffunc F(Element of X) = z * (f/.\$1); defpred P[set] means \$1 in dom f; set M = dom f; func z(#)f -> PartFunc of X,V means :Def2: dom it = dom f & for x be Element of X st x in dom it holds it/.x = z * (f/.x); existence proof consider F be PartFunc of X,V such that A1: for x be Element of X holds x in dom F iff P[x] and A2: for x be Element of X st x in dom F holds F/.x = F(x) from PARTFUN2:sch 2; take F; thus dom F = dom f by A1,SUBSET_1:3; let x be Element of X; assume x in dom F; hence thesis by A2; end; uniqueness proof thus for f,g being PartFunc of X,V st (dom f=M & for x be Element of X st x in dom f holds f/.x = F(x)) & (dom g=M & for x be Element of X st x in dom g holds g/.x = F(x)) holds f = g from PARTFUN2:sch 3; end; end; theorem for f1 be PartFunc of M,COMPLEX, f2 be PartFunc of M,V holds dom (f1(#)f2) \ (f1(#)f2)"{0.V} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{ 0.V}) proof let f1 be PartFunc of M,COMPLEX; let f2 be PartFunc of M,V; thus dom (f1(#)f2) \ (f1(#)f2)"{0.V} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2 )"{0.V}) proof let x be object; assume A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0.V}; then reconsider x1=x as Element of M; A2: x in dom (f1(#)f2) by A1,XBOOLE_0:def 5; then A3: x1 in dom f1 /\ dom f2 by Def1; not x in (f1(#)f2)"{0.V} by A1,XBOOLE_0:def 5; then not (f1(#)f2)/.x1 in {0.V} by A2,PARTFUN2:26; then (f1(#)f2)/.x1 <> 0.V by TARSKI:def 1; then A4: (f1/.x1) * (f2/.x1) <> 0.V by A2,Def1; then (f1/.x1) <> 0c by CLVECT_1:1; then A5: not f1/.x1 in {0} by TARSKI:def 1; (f2/.x1) <> 0.V by A4,CLVECT_1:1; then not (f2/.x1) in {0.V} by TARSKI:def 1; then A6: not x1 in (f2)"{0.V} by PARTFUN2:26; x1 in dom f2 by A3,XBOOLE_0:def 4; then A7: x in dom f2 \ (f2)"{0.V} by A6,XBOOLE_0:def 5; x1 in dom f1 by A3,XBOOLE_0:def 4; then not f1.x1 in {0} by A5,PARTFUN1:def 6; then A8: not x1 in (f1)"{0} by FUNCT_1:def 7; x1 in dom f1 by A3,XBOOLE_0:def 4; then x in dom f1 \ (f1)"{0} by A8,XBOOLE_0:def 5; hence thesis by A7,XBOOLE_0:def 4; end; thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) c= dom (f1(#)f2) \ (f1(#) f2)"{0.V} proof let x be object; assume A9: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}); then reconsider x1=x as Element of M; A10: x in dom f1 \ (f1)"{0} by A9,XBOOLE_0:def 4; then A11: x in dom f1 by XBOOLE_0:def 5; not x in (f1)"{0} by A10,XBOOLE_0:def 5; then not f1.x1 in {0} by A11,FUNCT_1:def 7; then f1.x1 <> 0 by TARSKI:def 1; then A12: f1/.x1 <> 0 by A11,PARTFUN1:def 6; A13: x in dom f2 \ (f2)"{0.V} by A9,XBOOLE_0:def 4; then A14: x in dom f2 by XBOOLE_0:def 5; then x1 in dom f1 /\ dom f2 by A11,XBOOLE_0:def 4; then A15: x1 in dom (f1(#)f2) by Def1; not x in (f2)"{0.V} by A13,XBOOLE_0:def 5; then not (f2/.x1) in {0.V} by A14,PARTFUN2:26; then (f2/.x1) <> 0.V by TARSKI:def 1; then f1/.x1 * (f2/.x1) <>0.V by A12,CLVECT_1:2; then (f1(#)f2)/.x1 <> 0.V by A15,Def1; then not (f1(#)f2)/.x1 in {0.V} by TARSKI:def 1; then not x in (f1(#)f2)"{0.V} by PARTFUN2:26; hence thesis by A15,XBOOLE_0:def 5; end; end; theorem (||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V} proof now let c be Element of M; thus c in (||.f.||)"{0} implies c in f"{0.V} proof assume A1: c in (||.f.||)"{0}; 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 thesis by A3,PARTFUN2:26; end; assume A4: c in (f)"{0.V}; then c in dom f by PARTFUN2:26; then A5: c in dom (||.f.||) by NORMSP_0:def 3; f/.c in {0.V} by A4,PARTFUN2:26; then f/.c = 0.V by TARSKI:def 1; then ||.f/.c.|| = 0 by NORMSP_0:def 6; then (||.f.||).c = 0 by A5,NORMSP_0:def 3; then (||.f.||).c in {0} by TARSKI:def 1; hence c in (||.f.||)"{0} by A5,FUNCT_1:def 7; end; hence (||.f.||)"{0} = f"{0.V} by SUBSET_1:3; now let c be Element of M; thus c in (-f)"{0.V} implies c in f"{0.V} proof assume A6: c in (-f)"{0.V}; then A7: c in dom (-f) by PARTFUN2:26; (-f)/.c in {0.V} by A6,PARTFUN2:26; then (-f)/.c = 0.V by TARSKI:def 1; then --(f/.c) = -0.V by A7,VFUNCT_1:def 5; then --(f/.c) = 0.V by RLVECT_1:12; then f/.c = 0.V by RLVECT_1:17; then A8: f/.c in {0.V} by TARSKI:def 1; c in dom f by A7,VFUNCT_1:def 5; hence thesis by A8,PARTFUN2:26; end; assume A9: c in (f)"{0.V}; then c in dom f by PARTFUN2:26; then A10: c in dom (-f) by VFUNCT_1:def 5; f/.c in {0.V} by A9,PARTFUN2:26; then f/.c = 0.V by TARSKI:def 1; then (-f)/.c = -0.V by A10,VFUNCT_1:def 5; then (-f)/.c = 0.V by RLVECT_1:12; then (-f)/.c in {0.V} by TARSKI:def 1; hence c in (-f)"{0.V} by A10,PARTFUN2:26; end; hence thesis by SUBSET_1:3; end; theorem z<>0c implies (z(#)f)"{0.V} = f"{0.V} proof assume A1: z<>0c; now let x be Element of M; thus x in (z(#)f)"{0.V} implies x in f"{0.V} proof assume A2: x in (z(#)f)"{0.V}; then A3: x in dom (z(#)f) by PARTFUN2:26; (z(#)f)/.x in {0.V} by A2,PARTFUN2:26; then (z(#)f)/.x = 0.V by TARSKI:def 1; then z*f/.x = 0.V by A3,Def2; then z*f/.x = z*0.V by CLVECT_1:1; then f/.x = 0.V by A1,CLVECT_1:11; then A4: f/.x in {0.V} by TARSKI:def 1; x in dom f by A3,Def2; hence thesis by A4,PARTFUN2:26; end; assume A5: x in (f)"{0.V}; then x in dom f by PARTFUN2:26; then A6: x in dom (z(#)f) by Def2; f/.x in {0.V} by A5,PARTFUN2:26; then z*f/.x = z*0.V by TARSKI:def 1; then z*f/.x = 0.V by CLVECT_1:1; then (z(#)f)/.x = 0.V by A6,Def2; then (z(#)f)/.x in {0.V} by TARSKI:def 1; hence x in (z(#)f)"{0.V} by A6,PARTFUN2:26; end; hence thesis by SUBSET_1:3; end; :: :: BASIC PROPERTIES OF OPERATIONS :: theorem Th4: f1 + f2 = f2 + f1 proof A1: dom (f1 + f2) = dom f2 /\ dom f1 by VFUNCT_1:def 1 .= dom (f2 + f1) by VFUNCT_1:def 1; now let x be Element of M; assume A2: x in dom (f1+f2); hence (f1 + f2)/.x = (f2/.x) + (f1/.x) by VFUNCT_1:def 1 .= (f2 + f1)/.x by A1,A2,VFUNCT_1:def 1; end; hence thesis by A1,PARTFUN2:1; end; definition let M,V; let f1,f2; redefine func f1+f2; commutativity by Th4; end; theorem (f1 + f2) + f3 = f1 + (f2 + f3) proof A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by VFUNCT_1:def 1 .= dom f1 /\ dom f2 /\ dom f3 by VFUNCT_1:def 1 .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom f1 /\ dom (f2 + f3) by VFUNCT_1:def 1 .= dom (f1 + (f2 + f3)) by VFUNCT_1:def 1; now let x be Element of M; assume A2: x in dom (f1 + f2 + f3); then x in dom (f1 + f2) /\ dom f3 by VFUNCT_1:def 1; then A3: x in dom (f1 + f2) by XBOOLE_0:def 4; x in dom f1 /\ dom (f2 + f3) by A1,A2,VFUNCT_1:def 1; then A4: x in dom (f2 + f3) by XBOOLE_0:def 4; thus (f1 + f2 + f3)/.x = ((f1 + f2)/.x) + (f3/.x) by A2,VFUNCT_1:def 1 .= (f1/.x) + (f2/.x) + (f3/.x) by A3,VFUNCT_1:def 1 .= (f1/.x) + ((f2/.x) + (f3/.x)) by RLVECT_1:def 3 .= (f1/.x) + ((f2 + f3)/.x) by A4,VFUNCT_1:def 1 .= (f1 + (f2 + f3))/.x by A1,A2,VFUNCT_1:def 1; end; hence thesis by A1,PARTFUN2:1; end; theorem for f1,f2 be PartFunc of M,COMPLEX,f3 be PartFunc of M,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) proof let f1,f2 be PartFunc of M,COMPLEX; let f3 be PartFunc of M,V; A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by Def1 .= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 4 .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom f1 /\ dom (f2 (#) f3) by Def1 .= dom (f1 (#) (f2 (#) f3)) by Def1; now let x be Element of M; assume A2: x in dom (f1(#)f2(#)f3); then x in dom (f1 (#) f2) /\ dom f3 by Def1; then A3: x in dom (f1 (#) f2) by XBOOLE_0:def 4; A4: dom (f1 (#) f2) = dom f1 /\ dom f2 by VALUED_1:def 4; then x in dom f1 by A3,XBOOLE_0:def 4; then A5: f1.x = f1/.x by PARTFUN1:def 6; x in dom f2 by A3,A4,XBOOLE_0:def 4; then A6: f2.x = f2/.x by PARTFUN1:def 6; A7: (f1 (#) f2)/.x = (f1 (#) f2).x by A3,PARTFUN1:def 6 .= f1/.x * f2/.x by A3,A5,A6,VALUED_1:def 4; x in dom f1 /\ dom (f2(#)f3) by A1,A2,Def1; then A8: x in dom (f2 (#) f3) by XBOOLE_0:def 4; thus (f1 (#) f2 (#) f3)/.x = (f1 (#) f2)/.x * (f3/.x) by A2,Def1 .= f1/.x * (f2/.x * (f3/.x)) by A7,CLVECT_1:def 4 .= f1/.x * ((f2 (#) f3)/.x) by A8,Def1 .= (f1 (#) (f2 (#) f3))/.x by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:1; end; theorem for f1,f2 be PartFunc of M,COMPLEX holds (f1 + f2) (#) f3 = f1 (#) f3 + f2 (#) f3 proof let f1,f2 be PartFunc of M,COMPLEX; A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by Def1 .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:def 1 .= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by Def1 .= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Def1 .= dom (f1 (#) f3 + f2 (#) f3) by VFUNCT_1:def 1; A2: dom (f1 + f2) = dom f1 /\ dom f2 by VALUED_1:def 1; now let x be Element of M; assume A3: x in dom ((f1 + f2)(#)f3); then A4: x in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,VFUNCT_1:def 1; then A5: x in dom (f1(#)f3) by XBOOLE_0:def 4; x in dom (f1 + f2) /\ dom f3 by A3,Def1; then A6: x in dom (f1 + f2) by XBOOLE_0:def 4; then x in dom f1 by A2,XBOOLE_0:def 4; then A7: f1/.x = f1.x by PARTFUN1:def 6; x in dom f2 by A2,A6,XBOOLE_0:def 4; then A8: f2/.x = f2.x by PARTFUN1:def 6; A9: (f1 + f2)/.x = (f1 + f2).x by A6,PARTFUN1:def 6 .= f1/.x + f2/.x by A6,A7,A8,VALUED_1:def 1; A10: x in dom (f2 (#) f3) by A4,XBOOLE_0:def 4; thus ((f1 + f2) (#) f3)/.x = (f1 + f2)/.x * (f3/.x) by A3,Def1 .= f1/.x * (f3/.x) + f2/.x * (f3/.x) by A9,CLVECT_1:def 3 .= ((f1 (#) f3)/.x) + f2/.x* (f3/.x) by A5,Def1 .= ((f1 (#) f3)/.x) + ((f2 (#) f3)/.x) by A10,Def1 .= ((f1 (#) f3) + (f2 (#) f3))/.x by A1,A3,VFUNCT_1:def 1; end; hence thesis by A1,PARTFUN2:1; end; theorem for f3 be PartFunc of M,COMPLEX holds f3(#)(f1 + f2) = f3(#)f1 + f3(#) f2 proof let f3 be PartFunc of M,COMPLEX; A1: dom (f3 (#) (f1 + f2)) = dom f3 /\ dom (f1 + f2) by Def1 .= dom f3 /\ (dom f1 /\ dom f2) by VFUNCT_1:def 1 .= dom f3 /\ dom f3 /\ dom f1 /\ dom f2 by XBOOLE_1:16 .= dom f3 /\ dom f1 /\ dom f3 /\ dom f2 by XBOOLE_1:16 .= dom f3 /\ dom f1 /\ (dom f3 /\ dom f2) by XBOOLE_1:16 .= dom (f3 (#) f1) /\ (dom f3 /\ dom f2) by Def1 .= dom (f3 (#) f1) /\ dom (f3 (#) f2) by Def1 .= dom (f3 (#) f1 + f3 (#) f2) by VFUNCT_1:def 1; now let x be Element of M; assume A2: x in dom (f3(#)(f1 + f2)); then x in dom f3 /\ dom (f1 + f2) by Def1; then A3: x in dom (f1 + f2) by XBOOLE_0:def 4; A4: x in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,A2,VFUNCT_1:def 1; then A5: x in dom (f3(#)f1) by XBOOLE_0:def 4; A6: x in dom (f3 (#) f2) by A4,XBOOLE_0:def 4; thus (f3 (#) (f1 + f2))/.x = f3/.x * ((f1 + f2)/.x) by A2,Def1 .= f3/.x * ((f1/.x) + (f2/.x)) by A3,VFUNCT_1:def 1 .= f3/.x * (f1/.x) + f3/.x * (f2/.x) by CLVECT_1:def 2 .= ((f3 (#) f1)/.x) + f3/.x* (f2/.x) by A5,Def1 .= ((f3 (#) f1)/.x) + ((f3 (#) f2)/.x) by A6,Def1 .= ((f3 (#) f1) + (f3 (#) f2))/.x by A1,A2,VFUNCT_1:def 1; end; hence thesis by A1,PARTFUN2:1; end; theorem for f1 be PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = z (#) f1 (#) f2 proof let f1 be PartFunc of M,COMPLEX; A1: dom (f1 (#) f2) = dom f1 /\ dom f2 by Def1; A2: dom (z(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def2 .= dom (z(#)f1) /\ dom f2 by A1,VALUED_1:def 5 .= dom (z(#)f1(#)f2) by Def1; now let x be Element of M; assume A3: x in dom (z(#)(f1(#)f2)); then x in dom (z(#)f1) /\ dom f2 by A2,Def1; then x in dom (z(#)f1) by XBOOLE_0:def 4; then A4: (z(#)f1)/.x = (z(#)f1).x by PARTFUN1:def 6; A5: x in dom (f1(#)f2) by A3,Def2; then x in dom f1 by A1,XBOOLE_0:def 4; then A6: f1/.x = f1.x by PARTFUN1:def 6; thus (z(#)(f1(#)f2))/.x = z * ((f1(#)f2)/.x) by A3,Def2 .= z*(f1/.x * (f2/.x)) by A5,Def1 .= (z*f1/.x) * (f2/.x) by CLVECT_1:def 4 .= (z(#)f1)/.x * (f2/.x) by A4,A6,VALUED_1:6 .= (z(#)f1 (#) f2)/.x by A2,A3,Def1; end; hence thesis by A2,PARTFUN2:1; end; theorem for f1 be PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2) proof let f1 be PartFunc of M,COMPLEX; A1: dom (z(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def2 .= dom f1 /\ dom f2 by Def1 .= dom f1 /\ dom (z(#)f2) by Def2 .= dom (f1(#)(z(#)f2)) by Def1; now let x be Element of M; assume A2: x in dom (z(#)(f1(#)f2)); then A3: x in dom (f1(#)f2) by Def2; x in dom f1 /\ dom (z(#)f2) by A1,A2,Def1; then A4: x in dom (z(#)f2) by XBOOLE_0:def 4; thus (z(#)(f1(#)f2))/.x = z * (f1(#)f2)/.x by A2,Def2 .= z * (f1/.x * (f2/.x)) by A3,Def1 .= f1/.x * z * (f2/.x) by CLVECT_1:def 4 .= f1/.x * (z * (f2/.x)) by CLVECT_1:def 4 .= f1/.x * ((z(#)f2)/.x) by A4,Def2 .= (f1(#)(z(#)f2))/.x by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:1; end; theorem for f1,f2 be PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = f1(#)f3 - f2(#)f3 proof let f1,f2 be PartFunc of M,COMPLEX; A1: dom ((f1 - f2) (#) f3) = dom (f1 + -f2) /\ dom f3 by Def1 .= dom f1 /\ dom (-f2) /\ (dom f3 /\ dom f3) by VALUED_1:def 1 .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:8 .= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by Def1 .= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Def1 .= dom (f1 (#) f3 - f2 (#) f3) by VFUNCT_1:def 2; now let x be Element of M; assume A2: x in dom ((f1 - f2)(#)f3); then A3: x in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,VFUNCT_1:def 2; then A4: x in dom (f1(#)f3) by XBOOLE_0:def 4; x in dom (f1 - f2) /\ dom f3 by A2,Def1; then A5: x in dom (f1 - f2) by XBOOLE_0:def 4; then A6: x in dom f1 /\ dom (-f2) by VALUED_1:def 1; then A7: x in dom (-f2) by XBOOLE_0:def 4; x in dom f1 by A6,XBOOLE_0:def 4; then A8: f1/.x = f1.x by PARTFUN1:def 6; (f1 + -f2)/.x = (f1 + -f2).x by A5,PARTFUN1:def 6; then A9: (f1 + -f2)/.x = f1.x + (-f2).x by A5,VALUED_1:def 1 .= f1/.x + (-f2)/.x by A7,A8,PARTFUN1:def 6; dom -f2 = dom f2 by VALUED_1:8; then A10: (-f2).x = -(f2.x) & f2/.x = f2.x by A7,PARTFUN1:def 6,VALUED_1:8; A11: x in dom (f2 (#) f3) by A3,XBOOLE_0:def 4; (-f2)/.x = (-f2).x by A7,PARTFUN1:def 6; hence ((f1 - f2) (#) f3)/.x = (f1/.x - f2/.x) * (f3/.x) by A2,A10,A9,Def1 .= f1/.x * (f3/.x) - f2/.x * (f3/.x) by CLVECT_1:10 .= ((f1 (#) f3)/.x) - f2/.x * (f3/.x) by A4,Def1 .= ((f1 (#) f3)/.x) - ((f2 (#) f3)/.x) by A11,Def1 .= ((f1 (#) f3) - (f2 (#) f3))/.x by A1,A2,VFUNCT_1:def 2; end; hence thesis by A1,PARTFUN2:1; end; theorem for f3 be PartFunc of M,COMPLEX holds f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) proof let f3 be PartFunc of M,COMPLEX; A1: dom (f3 (#) f1 - f3 (#) f2) = dom (f3 (#) f1) /\ dom (f3 (#) f2) by VFUNCT_1:def 2 .= dom (f3 (#) f1) /\ (dom f3 /\ dom f2) by Def1 .= dom f3 /\ dom f1 /\ (dom f3 /\ dom f2) by Def1 .= dom f3 /\ (dom f3 /\ dom f1) /\ dom f2 by XBOOLE_1:16 .= dom f3 /\ dom f3 /\ dom f1 /\ dom f2 by XBOOLE_1:16 .= dom f3 /\ (dom f1 /\ dom f2) by XBOOLE_1:16 .= dom f3 /\ dom (f1 - f2) by VFUNCT_1:def 2 .= dom (f3(#)(f1 - f2)) by Def1; now let x be Element of M; assume A2: x in dom (f3(#)(f1 - f2)); then x in dom f3 /\ dom (f1 - f2) by Def1; then A3: x in dom (f1 - f2) by XBOOLE_0:def 4; A4: x in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,A2,VFUNCT_1:def 2; then A5: x in dom (f3(#)f1) by XBOOLE_0:def 4; A6: x in dom (f3 (#) f2) by A4,XBOOLE_0:def 4; thus (f3 (#) (f1 - f2))/.x = f3/.x * ((f1 - f2)/.x) by A2,Def1 .= f3/.x * ((f1/.x) - (f2/.x)) by A3,VFUNCT_1:def 2 .= f3/.x * (f1/.x) - f3/.x * (f2/.x) by CLVECT_1:9 .= ((f3 (#) f1)/.x) - f3/.x * (f2/.x) by A5,Def1 .= ((f3 (#) f1)/.x) - ((f3 (#) f2)/.x) by A6,Def1 .= ((f3 (#) f1) - (f3 (#) f2))/.x by A1,A2,VFUNCT_1:def 2; end; hence thesis by A1,PARTFUN2:1; end; theorem z(#)(f1 + f2) = z(#)f1 + z(#)f2 proof A1: dom (z(#)(f1 + f2)) = dom (f1 + f2) by Def2 .= dom f1 /\ dom f2 by VFUNCT_1:def 1 .= dom f1 /\ dom (z(#)f2) by Def2 .= dom (z(#)f1) /\ dom (z(#)f2) by Def2 .= dom (z(#)f1 + z(#)f2) by VFUNCT_1:def 1; now let x be Element of M; assume A2: x in dom (z(#)(f1 + f2)); then A3: x in dom (f1 + f2) by Def2; A4: x in dom (z(#)f1) /\ dom (z(#)f2) by A1,A2,VFUNCT_1:def 1; then A5: x in dom (z(#)f1) by XBOOLE_0:def 4; A6: x in dom (z(#)f2) by A4,XBOOLE_0:def 4; thus (z(#)(f1 + f2))/.x = z * ((f1 + f2)/.x) by A2,Def2 .= z * ((f1/.x) + (f2/.x)) by A3,VFUNCT_1:def 1 .= z * (f1/.x) + z * (f2/.x) by CLVECT_1:def 2 .= ((z(#)f1)/.x) + z * (f2/.x) by A5,Def2 .= ((z(#)f1)/.x) + ((z(#)f2)/.x) by A6,Def2 .= (z(#)f1 + z(#)f2)/.x by A1,A2,VFUNCT_1:def 1; end; hence thesis by A1,PARTFUN2:1; end; theorem Th14: (z1*z2)(#)f = z1(#)(z2(#)f) proof A1: dom ((z1*z2) (#) f) = dom f by Def2 .= dom (z2(#)f) by Def2 .= dom (z1(#)(z2(#)f)) by Def2; now let x be Element of M; assume A2: x in dom ((z1*z2)(#)f); then A3: x in dom (z2(#)f) by A1,Def2; thus ((z1*z2)(#)f)/.x = z1*z2 * f/.x by A2,Def2 .= z1*(z2 * f/.x) by CLVECT_1:def 4 .= z1 * ((z2(#)f)/.x) by A3,Def2 .= (z1(#)(z2(#)f))/.x by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:1; end; theorem z(#)(f1 - f2) = z(#)f1 - z(#)f2 proof A1: dom (z(#)(f1 - f2)) = dom (f1 - f2) by Def2 .= dom f1 /\ dom f2 by VFUNCT_1:def 2 .= dom f1 /\ dom (z(#)f2) by Def2 .= dom (z(#)f1) /\ dom (z(#)f2) by Def2 .= dom (z(#)f1 - z(#)f2) by VFUNCT_1:def 2; now let x be Element of M; assume A2: x in dom (z(#)(f1 - f2)); then A3: x in dom (f1 - f2) by Def2; A4: x in dom (z(#)f1) /\ dom (z(#)f2) by A1,A2,VFUNCT_1:def 2; then A5: x in dom (z(#)f1) by XBOOLE_0:def 4; A6: x in dom (z(#)f2) by A4,XBOOLE_0:def 4; thus (z(#)(f1 - f2))/.x = z * ((f1 - f2)/.x) by A2,Def2 .= z * ((f1/.x) - (f2/.x)) by A3,VFUNCT_1:def 2 .= z * (f1/.x) - z * (f2/.x) by CLVECT_1:9 .= ((z(#)f1)/.x) - z * (f2/.x) by A5,Def2 .= ((z(#)f1)/.x) - ((z(#)f2)/.x) by A6,Def2 .= (z(#)f1 - z(#)f2)/.x by A1,A2,VFUNCT_1:def 2; end; hence thesis by A1,PARTFUN2:1; end; theorem f1-f2 = (-1r)(#)(f2-f1) proof A1: dom (f1 - f2) = dom f2 /\ dom f1 by VFUNCT_1:def 2 .= dom (f2 - f1) by VFUNCT_1:def 2 .= dom ((-1r)(#)(f2 - f1)) by Def2; now A2: dom (f1 - f2) = dom f2 /\ dom f1 by VFUNCT_1:def 2 .= dom (f2 - f1) by VFUNCT_1:def 2; let x be Element of M such that A3: x in dom (f1-f2); thus (f1 - f2)/.x = (f1/.x) - (f2/.x) by A3,VFUNCT_1:def 2 .= -((f2/.x) - (f1/.x)) by RLVECT_1:33 .= (-1r)*((f2/.x) - (f1/.x)) by CLVECT_1:3 .= (-1r)*((f2 - f1)/.x) by A3,A2,VFUNCT_1:def 2 .= ((-1r)(#)(f2 - f1))/.x by A1,A3,Def2; end; hence thesis by A1,PARTFUN2:1; end; theorem f1 - (f2 + f3) = f1 - f2 - f3 proof A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by VFUNCT_1:def 2 .= dom f1 /\ (dom f2 /\ dom f3) by VFUNCT_1:def 1 .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom (f1 - f2) /\ dom f3 by VFUNCT_1:def 2 .= dom (f1 - f2 - f3) by VFUNCT_1:def 2; now let x be Element of M; assume A2: x in dom (f1 - (f2 + f3)); then x in dom f1 /\ dom (f2 + f3) by VFUNCT_1:def 2; then A3: x in dom (f2 + f3) by XBOOLE_0:def 4; x in dom (f1 - f2) /\ dom f3 by A1,A2,VFUNCT_1:def 2; then A4: x in dom (f1 - f2) by XBOOLE_0:def 4; thus (f1 - (f2 + f3))/.x = (f1/.x) - ((f2 + f3)/.x) by A2,VFUNCT_1:def 2 .= (f1/.x) - ((f2/.x) + (f3/.x)) by A3,VFUNCT_1:def 1 .= (f1/.x) - (f2/.x) - (f3/.x) by RLVECT_1:27 .= ((f1 - f2)/.x) - (f3/.x) by A4,VFUNCT_1:def 2 .= (f1 - f2 - f3)/.x by A1,A2,VFUNCT_1:def 2; end; hence thesis by A1,PARTFUN2:1; end; theorem Th18: 1r(#)f = f proof A1: now let c be Element of M; assume c in dom (1r(#)f); hence (1r(#)f)/.c = 1r * f/.c by Def2 .= f/.c by CLVECT_1:def 5; end; dom (1r(#)f) = dom f by Def2; hence thesis by A1,PARTFUN2:1; end; theorem f1 - (f2 - f3) = f1 - f2 + f3 proof A1: dom (f1 - (f2 - f3)) = dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 2 .= dom f1 /\ (dom f2 /\ dom f3) by VFUNCT_1:def 2 .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom (f1 - f2) /\ dom f3 by VFUNCT_1:def 2 .= dom (f1 - f2 + f3) by VFUNCT_1:def 1; now let c be Element of M; assume A2: c in dom (f1 - (f2 - f3)); then c in dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 2; then A3: c in dom (f2 - f3) by XBOOLE_0:def 4; c in dom (f1 - f2) /\ dom f3 by A1,A2,VFUNCT_1:def 1; then A4: c in dom (f1 - f2) by XBOOLE_0:def 4; thus (f1 - (f2 - f3))/.c = (f1/.c) - ((f2 - f3)/.c) by A2,VFUNCT_1:def 2 .= (f1/.c) - ((f2/.c) - (f3/.c)) by A3,VFUNCT_1:def 2 .= (f1/.c) - (f2/.c) + (f3/.c) by RLVECT_1:29 .= ((f1 - f2)/.c) + (f3/.c) by A4,VFUNCT_1:def 2 .= (f1 - f2 + f3)/.c by A1,A2,VFUNCT_1:def 1; end; hence thesis by A1,PARTFUN2:1; end; theorem f1 + (f2 - f3) = f1 + f2 - f3 proof A1: dom (f1 + (f2 - f3)) = dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 1 .= dom f1 /\ (dom f2 /\ dom f3) by VFUNCT_1:def 2 .= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16 .= dom (f1 + f2) /\ dom f3 by VFUNCT_1:def 1 .= dom (f1 + f2 - f3) by VFUNCT_1:def 2; now let c be Element of M; assume A2: c in dom (f1 + (f2 - f3)); then c in dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 1; then A3: c in dom (f2 - f3) by XBOOLE_0:def 4; c in dom (f1 + f2) /\ dom f3 by A1,A2,VFUNCT_1:def 2; then A4: c in dom (f1 + f2) by XBOOLE_0:def 4; thus (f1 + (f2 - f3))/.c = (f1/.c) + ((f2 - f3)/.c) by A2,VFUNCT_1:def 1 .= (f1/.c) + ((f2/.c) - (f3/.c)) by A3,VFUNCT_1:def 2 .= (f1/.c) + (f2/.c) - (f3/.c) by RLVECT_1:def 3 .= ((f1 + f2)/.c) - (f3/.c) by A4,VFUNCT_1:def 1 .= (f1 + f2 - f3)/.c by A1,A2,VFUNCT_1:def 2; end; hence thesis by A1,PARTFUN2:1; end; theorem for f1 be PartFunc of M,COMPLEX holds ||.f1(#)f2.|| = |.f1.|(#)||.f2 .|| proof let f1 be PartFunc of M,COMPLEX; A1: dom (f1 (#) f2) = dom f1 /\ dom f2 by Def1; A2: dom f1 /\ dom f2 = dom f1 /\ dom (||.f2.||) by NORMSP_0:def 3 .= dom (|.f1.|) /\ dom (||.f2.||) by VALUED_1:def 11 .= dom (|.f1.|(#)||.f2.||) by VALUED_1:def 4; A3: dom (||.f1 (#) f2.||) = dom (f1 (#) f2) by NORMSP_0:def 3; now let c be Element of M; assume A4: c in dom (||.f1 (#) f2.||); then c in dom (|.f1.|) /\ dom (||.f2.||) by A3,A1,A2,VALUED_1:def 4; then A5: c in dom (||.f2.||) by XBOOLE_0:def 4; A6: c in dom (f1 (#) f2) by A4,NORMSP_0:def 3; then c in dom f1 by A1,XBOOLE_0:def 4; then A7: f1/.c = f1.c by PARTFUN1:def 6; thus (||.f1(#)f2.||).c = ||.(f1(#)f2)/.c.|| by A4,NORMSP_0:def 3 .= ||.f1/.c * (f2/.c).|| by A6,Def1 .= |.(f1/.c).| * ||.(f2/.c).|| by CLVECT_1:def 13 .= ((|.f1.|).c) * ||.(f2/.c).|| by A7,VALUED_1:18 .= ((|.f1.|).c) * (||.f2.||).c by A5,NORMSP_0:def 3 .= (|.f1.|(#)||.f2.||).c by VALUED_1:5; end; hence thesis by A3,A1,A2,PARTFUN1:5; end; theorem ||.z(#)f.|| = |.z.|(#)||.f.|| proof A1: dom (||.z(#)f.||) = dom (z(#)f) by NORMSP_0:def 3 .= dom f by Def2 .= dom (||.f.||) by NORMSP_0:def 3 .= dom (|.z.|(#)||.f.||) by VALUED_1:def 5; now let c be Element of M; assume A2: c in dom (||.z(#)f.||); then A3: c in dom (||.f.||) by A1,VALUED_1:def 5; A4: c in dom (z(#)f) by A2,NORMSP_0:def 3; thus (||.z(#)f.||).c = ||.(z(#)f)/.c.|| by A2,NORMSP_0:def 3 .=||.z*(f/.c).|| by A4,Def2 .=|.z.|*||.f/.c.|| by CLVECT_1:def 13 .=|.z.|*(||.f.||.c) by A3,NORMSP_0:def 3 .=(|.z.|(#)||.f.||).c by A1,A2,VALUED_1:def 5; end; hence thesis by A1,PARTFUN1:5; end; theorem Th23: -f = (-1r)(#)f proof A1: dom (-f) = dom f by VFUNCT_1:def 5 .= dom ((-1r)(#)f) by Def2; now let c be Element of M; assume A2: c in dom ((-1r)(#)f); hence (-f)/.c = -(f/.c) by A1,VFUNCT_1:def 5 .= (-1r) * f/.c by CLVECT_1:3 .= ((-1r)(#)f)/.c by A2,Def2; end; hence thesis by A1,PARTFUN2:1; end; theorem Th24: -(-f) = f proof thus -(-f) = (-1r)(#)(-f) by Th23 .= (-1r)(#)((-1r)(#)f) by Th23 .= ((-1r)*(-1r))(#)f by Th14 .= f by Th18,COMPLEX1:def 4; end; theorem Th25: f1 - f2 = f1 + -f2 proof A1: dom (f1 - f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2 .= dom f1 /\ dom (-f2) by VFUNCT_1:def 5 .= dom (f1 + -f2) by VFUNCT_1:def 1; now let c be Element of M; assume A2: c in dom (f1+-f2); then c in dom f1 /\ dom (-f2) by VFUNCT_1:def 1; then A3: c in dom (-f2) by XBOOLE_0:def 4; thus (f1 + -f2)/.c = (f1/.c) + ((-f2)/.c) by A2,VFUNCT_1:def 1 .= (f1/.c) - (f2/.c) by A3,VFUNCT_1:def 5 .= (f1-f2)/.c by A1,A2,VFUNCT_1:def 2; end; hence thesis by A1,PARTFUN2:1; end; theorem f1 - (-f2) = f1 + f2 proof thus f1 - (-f2) = f1 + (-(-f2)) by Th25 .= f1 + f2 by Th24; end; reserve X,Y for set; theorem Th27: (f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X proof A1: now let c be Element of M; assume A2: c in dom ((f1+f2)|X); then A3: c in dom (f1+f2) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def 4; A5: c in dom (f1+f2) by A3,XBOOLE_0:def 4; then A6: c in dom f1 /\ dom f2 by VFUNCT_1:def 1; then c in dom f2 by XBOOLE_0:def 4; then c in dom f2 /\ X by A4,XBOOLE_0:def 4; then A7: c in dom (f2|X) by RELAT_1:61; c in dom f1 by A6,XBOOLE_0:def 4; then c in dom f1 /\ X by A4,XBOOLE_0:def 4; then A8: c in dom (f1|X) by RELAT_1:61; then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4; then A9: c in dom ((f1|X) + (f2|X)) by VFUNCT_1:def 1; thus ((f1+f2)|X)/.c = (f1+f2)/.c by A2,PARTFUN2:15 .= (f1/.c) + (f2/.c) by A5,VFUNCT_1:def 1 .= ((f1|X)/.c) + (f2/.c) by A8,PARTFUN2:15 .= ((f1|X)/.c) + ((f2|X)/.c) by A7,PARTFUN2:15 .= ((f1|X)+(f2|X))/.c by A9,VFUNCT_1:def 1; end; dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61 .= dom f1 /\ dom f2 /\ (X /\ X) by VFUNCT_1:def 1 .= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16 .= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16 .= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61 .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16 .= dom (f1|X) /\ dom (f2|X) by RELAT_1:61 .= dom ((f1|X)+(f2|X)) by VFUNCT_1:def 1; hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN2:1; A10: now let c be Element of M; assume A11: c in dom ((f1+f2)|X); then A12: c in dom (f1+f2) /\ X by RELAT_1:61; then A13: c in X by XBOOLE_0:def 4; A14: c in dom (f1+f2) by A12,XBOOLE_0:def 4; then A15: c in dom f1 /\ dom f2 by VFUNCT_1:def 1; then c in dom f1 by XBOOLE_0:def 4; then c in dom f1 /\ X by A13,XBOOLE_0:def 4; then A16: c in dom (f1|X) by RELAT_1:61; c in dom f2 by A15,XBOOLE_0:def 4; then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4; then A17: c in dom ((f1|X) + f2) by VFUNCT_1:def 1; thus ((f1+f2)|X)/.c = (f1+f2)/.c by A11,PARTFUN2:15 .= (f1/.c) + (f2/.c) by A14,VFUNCT_1:def 1 .= ((f1|X)/.c) +(f2/.c) by A16,PARTFUN2:15 .= ((f1|X)+f2)/.c by A17,VFUNCT_1:def 1; end; dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61 .= dom f1 /\ dom f2 /\ X by VFUNCT_1:def 1 .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16 .= dom (f1|X) /\ dom f2 by RELAT_1:61 .= dom ((f1|X)+ f2) by VFUNCT_1:def 1; hence (f1+f2)|X = f1|X + f2 by A10,PARTFUN2:1; A18: now let c be Element of M; assume A19: c in dom ((f1+f2)|X); then A20: c in dom (f1+f2) /\ X by RELAT_1:61; then A21: c in X by XBOOLE_0:def 4; A22: c in dom (f1+f2) by A20,XBOOLE_0:def 4; then A23: c in dom f1 /\ dom f2 by VFUNCT_1:def 1; then c in dom f2 by XBOOLE_0:def 4; then c in dom f2 /\ X by A21,XBOOLE_0:def 4; then A24: c in dom (f2|X) by RELAT_1:61; c in dom f1 by A23,XBOOLE_0:def 4; then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4; then A25: c in dom (f1 + (f2|X)) by VFUNCT_1:def 1; thus ((f1+f2)|X)/.c = (f1+f2)/.c by A19,PARTFUN2:15 .= (f1/.c) +(f2/.c) by A22,VFUNCT_1:def 1 .= (f1/.c) + ((f2|X)/.c) by A24,PARTFUN2:15 .= (f1+(f2|X))/.c by A25,VFUNCT_1:def 1; end; dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61 .= dom f1 /\ dom f2 /\ X by VFUNCT_1:def 1 .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16 .= dom f1 /\ dom (f2|X) by RELAT_1:61 .= dom (f1 + (f2|X)) by VFUNCT_1:def 1; hence thesis by A18,PARTFUN2:1; end; theorem for f1 be PartFunc of M,COMPLEX holds (f1(#)f2)|X = f1|X (#) f2|X & ( f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#) f2|X proof let f1 be PartFunc of M,COMPLEX; A1: now let c be Element of M; assume A2: c in dom ((f1(#)f2)|X); then A3: c in dom (f1(#)f2) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def 4; A5: c in dom (f1(#)f2) by A3,XBOOLE_0:def 4; then A6: c in dom f1 /\ dom f2 by Def1; then A7: c in dom f1 by XBOOLE_0:def 4; then c in dom f1 /\ X by A4,XBOOLE_0:def 4; then A8: c in dom (f1|X) by RELAT_1:61; then A9: (f1|X)/.c = (f1|X).c by PARTFUN1:def 6 .= f1.c by A8,FUNCT_1:47 .= f1/.c by A7,PARTFUN1:def 6; c in dom f2 by A6,XBOOLE_0:def 4; then c in dom f2 /\ X by A4,XBOOLE_0:def 4; then A10: c in dom (f2|X) by RELAT_1:61; then c in dom (f1|X) /\ dom (f2|X) by A8,XBOOLE_0:def 4; then A11: c in dom ((f1|X) (#) (f2|X)) by Def1; thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A2,PARTFUN2:15 .= (f1/.c) * (f2/.c) by A5,Def1 .= ((f1|X)/.c) * ((f2|X)/.c) by A10,A9,PARTFUN2:15 .= ((f1|X)(#)(f2|X))/.c by A11,Def1; 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; A12: now let c be Element of M; assume A13: c in dom ((f1(#)f2)|X); then A14: c in dom (f1(#)f2) /\ X by RELAT_1:61; then A15: c in dom (f1(#)f2) by XBOOLE_0:def 4; then A16: c in dom f1 /\ dom f2 by Def1; then A17: c in dom f1 by XBOOLE_0:def 4; c in X by A14,XBOOLE_0:def 4; then c in dom f1 /\ X by A17,XBOOLE_0:def 4; then A18: c in dom (f1|X) by RELAT_1:61; then A19: (f1|X)/.c = (f1|X).c by PARTFUN1:def 6 .= f1.c by A18,FUNCT_1:47; c in dom f2 by A16,XBOOLE_0:def 4; then c in dom (f1|X) /\ dom f2 by A18,XBOOLE_0:def 4; then A20: c in dom ((f1|X) (#) f2) by Def1; thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A13,PARTFUN2:15 .= (f1/.c) * (f2/.c) by A15,Def1 .= ((f1|X)/.c) * (f2/.c) by A17,A19,PARTFUN1:def 6 .= ((f1|X)(#)f2)/.c by A20,Def1; end; dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61 .= dom f1 /\ dom f2 /\ X by Def1 .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16 .= dom (f1|X) /\ dom f2 by RELAT_1:61 .= dom ((f1|X)(#) f2) by Def1; hence (f1(#)f2)|X = f1|X (#) f2 by A12,PARTFUN2:1; A21: now let c be Element of M; assume A22: c in dom ((f1(#)f2)|X); then A23: c in dom (f1(#)f2) /\ X by RELAT_1:61; then A24: c in X by XBOOLE_0:def 4; A25: c in dom (f1(#)f2) by A23,XBOOLE_0:def 4; then A26: c in dom f1 /\ dom f2 by Def1; then c in dom f2 by XBOOLE_0:def 4; then c in dom f2 /\ X by A24,XBOOLE_0:def 4; then A27: c in dom (f2|X) by RELAT_1:61; c in dom f1 by A26,XBOOLE_0:def 4; then c in dom f1 /\ dom (f2|X) by A27,XBOOLE_0:def 4; then A28: c in dom (f1 (#) (f2|X)) by Def1; thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A22,PARTFUN2:15 .= (f1/.c) * (f2/.c) by A25,Def1 .= (f1/.c) * ((f2|X)/.c) by A27,PARTFUN2:15 .= (f1(#)(f2|X))/.c by A28,Def1; 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 thesis by A21,PARTFUN2:1; end; theorem Th29: (-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).|| proof A1: now let c be Element of M; assume A2: c in dom ((-f)|X); then A3: c in dom (-f) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def 4; A5: c in dom (-f) by A3,XBOOLE_0:def 4; then c in dom f by VFUNCT_1:def 5; then c in dom f /\ X by A4,XBOOLE_0:def 4; then A6: c in dom (f|X) by RELAT_1:61; then A7: c in dom (-(f|X)) by VFUNCT_1:def 5; thus ((-f)|X)/.c = (-f)/.c by A2,PARTFUN2:15 .= -(f/.c) by A5,VFUNCT_1:def 5 .= -((f|X)/.c) by A6,PARTFUN2:15 .= (-(f|X))/.c by A7,VFUNCT_1:def 5; end; dom ((-f)|X) = dom (-f) /\ X by RELAT_1:61 .= dom f /\ X by VFUNCT_1:def 5 .= dom (f|X) by RELAT_1:61 .= dom (-(f|X)) by VFUNCT_1:def 5; hence (-f)|X = -(f|X) by A1,PARTFUN2:1; 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 let c be Element of M; assume A9: c in dom ((||.f.||)|X); 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; end; hence thesis by A8,PARTFUN1:5; end; theorem (f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X proof 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; thus (f1-f2)|X = (f1+-f2)|X by Th25 .= (f1|X)+ -f2 by Th27 .= (f1|X) - f2 by Th25; thus (f1-f2)|X = (f1+-f2)|X by Th25 .= f1+ (-f2)|X by Th27 .= f1 +- (f2|X) by Th29 .= f1 - (f2|X) by Th25; end; theorem (z(#)f)|X = z(#)(f|X) proof A1: now let c be Element of M; assume A2: c in dom ((z(#)f)|X); then A3: c in dom (z(#)f) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def 4; A5: c in dom (z(#)f) by A3,XBOOLE_0:def 4; then c in dom f by Def2; then c in dom f /\ X by A4,XBOOLE_0:def 4; then A6: c in dom (f|X) by RELAT_1:61; then A7: c in dom (z(#)(f|X)) by Def2; thus ((z(#)f)|X)/.c = (z(#)f)/.c by A2,PARTFUN2:15 .= z*(f/.c) by A5,Def2 .= z*((f|X)/.c) by A6,PARTFUN2:15 .= (z(#)(f|X))/.c by A7,Def2; end; dom ((z(#)f)|X) = dom (z(#)f) /\ X by RELAT_1:61 .= dom f /\ X by Def2 .= dom (f|X) by RELAT_1:61 .= dom (z(#)(f|X)) by Def2; hence thesis by A1,PARTFUN2:1; end; :: :: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX :: theorem Th32: (f1 is total & f2 is total iff f1+f2 is total) & (f1 is total & f2 is total iff f1-f2 is total) proof thus f1 is total & f2 is total iff f1+f2 is total proof thus f1 is total & f2 is total implies f1+f2 is total proof assume f1 is total & f2 is total; then dom f1 = M & dom f2 = M; hence dom (f1+f2) = M /\ M by VFUNCT_1:def 1 .= M; end; assume f1+f2 is total; then dom (f1+f2) = M; then dom f1 /\ dom f2 = M by VFUNCT_1:def 1; then M c= dom f1 & M c= dom f2 by XBOOLE_1:17; hence dom f1 = M & dom f2 = M; end; thus f1 is total & f2 is total iff f1-f2 is total proof thus f1 is total & f2 is total implies f1-f2 is total proof assume f1 is total & f2 is total; then dom f1 = M & dom f2 = M; hence dom (f1-f2) = M /\ M by VFUNCT_1:def 2 .= M; end; assume f1-f2 is total; then dom (f1-f2) = M; then dom f1 /\ dom f2 = M by VFUNCT_1:def 2; then M c= dom f1 & M c= dom f2 by XBOOLE_1:17; hence dom f1 = M & dom f2 = M; end; end; theorem Th33: for f1 be PartFunc of M,COMPLEX holds (f1 is total & f2 is total iff f1(#)f2 is total) proof let f1 be PartFunc of M,COMPLEX; thus f1 is total & f2 is total implies f1(#)f2 is total proof assume f1 is total & f2 is total; then dom f1 = M & dom f2 = M; hence dom (f1(#)f2) = M /\ M by Def1 .= M; end; assume f1(#)f2 is total; then dom (f1(#)f2) = M; then dom f1 /\ dom f2 = M by Def1; then M c= dom f1 & M c= dom f2 by XBOOLE_1:17; hence dom f1 = M & dom f2 = M; end; theorem Th34: f is total iff z(#)f is total by Def2; theorem Th35: f is total iff -f is total proof thus f is total implies -f is total proof assume A1: f is total; -f = (-1r)(#)f by Th23; hence thesis by A1,Th34; end; assume A2: -f is total; -f = (-1r)(#)f by Th23; hence thesis by A2,Th34; end; theorem Th36: f is total iff ||.f.|| is total by NORMSP_0:def 3; theorem for x be Element of M st f1 is total & f2 is total holds (f1+f2)/.x = (f1/.x) + (f2/.x) & (f1-f2)/.x = (f1/.x) - (f2/.x) proof let x be Element of M; assume A1: f1 is total & f2 is total; then f1+f2 is total by Th32; then dom (f1+f2) = M; hence (f1+f2)/.x = (f1/.x) + (f2/.x) by VFUNCT_1:def 1; f1-f2 is total by A1,Th32; then dom (f1-f2) = M; hence thesis by VFUNCT_1:def 2; end; theorem for f1 be PartFunc of M,COMPLEX, x be Element of M holds f1 is total & f2 is total implies (f1(#)f2)/.x = f1/.x * (f2/.x) proof let f1 be PartFunc of M,COMPLEX; let x be Element of M; assume f1 is total & f2 is total; then f1(#)f2 is total by Th33; then dom (f1(#)f2) = M; hence thesis by Def1; end; theorem for x be Element of M st f is total holds (z(#)f)/.x = z * (f/.x) proof let x be Element of M; assume f is total; then z(#)f is total by Th34; then dom (z(#)f) = M; hence thesis by Def2; end; theorem for x be Element of M st f is total holds (-f)/.x = - f/.x & (||.f.||) .x = ||. f/.x .|| proof let x be Element of M; assume A1: f is total; then -f is total by Th35; then dom (-f) = M; hence (-f)/.x = - f/.x by VFUNCT_1:def 5; ||.f.|| is total by A1,Th36; then dom (||.f.||) = M; hence thesis by NORMSP_0:def 3; end; :: :: BOUNDED AND CONSTANT PARTIAL FUNCTIONS :: FROM A DOMAIN TO A NORMED COMPLEX SPACE :: definition let M; let V; let f,Y; pred f is_bounded_on Y means ex r be Real st for x be Element of M st x in Y /\ dom f holds ||.f/.x.|| <= r; end; theorem Y c= X & f is_bounded_on X implies f is_bounded_on Y proof assume that A1: Y c= X and A2: f is_bounded_on X; consider r be Real such that A3: for x be Element of M st x in X /\ dom f holds ||.f/.x.|| <= r by A2; take r; let x be Element of M; assume x in Y /\ dom f; then x in Y & x in dom f by XBOOLE_0:def 4; then x in X /\ dom f by A1,XBOOLE_0:def 4; hence thesis by A3; end; theorem X misses dom f implies f is_bounded_on X proof assume X /\ dom f = {}; then for x be Element of M holds x in X /\ dom f implies ||.f/.x.|| <= 0; hence thesis; end; theorem 0c(#)f is_bounded_on Y proof now take p=0; let c be Element of M; |.0c.|*||.f/.c.|| <= 0 by COMPLEX1:44; then A1: ||.0c*(f/.c).|| <= 0 by CLVECT_1:def 13; assume c in Y /\ dom (0c(#)f); then c in dom (0c(#)f) by XBOOLE_0:def 4; hence ||.(0c(#)f)/.c.|| <= p by A1,Def2; end; hence thesis; end; theorem Th44: f is_bounded_on Y implies z(#)f is_bounded_on Y proof assume f is_bounded_on Y; then consider r1 be Real such that A1: for c be Element of M st c in Y /\ dom f holds ||.f/.c.|| <= r1; reconsider p = |.z.|*|.r1.| as Real; take p; let c be Element of M; assume A2: c in Y /\ dom (z(#)f); then A3: c in Y by XBOOLE_0:def 4; A4: c in dom (z(#)f) by A2,XBOOLE_0:def 4; then c in dom f by Def2; then c in Y /\ dom f by A3,XBOOLE_0:def 4; then A5: ||.f/.c.|| <= r1 by A1; r1 <= |.r1.| by ABSVALUE:4; then |.z.| >= 0 & ||.f/.c.|| <= |.r1.| by A5,COMPLEX1:46,XXREAL_0:2; then |.z.| * ||.(f/.c).|| <= |.z.|*|.r1.| by XREAL_1:64; then ||.z * (f/.c).|| <= p by CLVECT_1:def 13; hence thesis by A4,Def2; end; theorem Th45: f is_bounded_on Y implies ||.f.|||Y is bounded & -f is_bounded_on Y proof assume A1: f is_bounded_on Y; then consider r1 be Real such that A2: for c be Element of M st c in Y /\ dom f holds ||.f/.c.|| <= r1; now let c be object; assume A3: c in Y /\ dom (||.f.||); then A4: c in Y by XBOOLE_0:def 4; A5: c in dom (||.f.||) by A3,XBOOLE_0:def 4; then c in dom f by NORMSP_0:def 3; then c in Y /\ dom f by A4,XBOOLE_0:def 4; then ||.f/.c.|| >= 0 & ||.f/.c.|| <= r1 by A2,CLVECT_1:105; then |.||.f/.c.||.| <= r1 by ABSVALUE:def 1; hence |.(||.f.||).c.| <= r1 by A5,NORMSP_0:def 3; end; hence ||.f.|||Y is bounded by RFUNCT_1:73; (-1r)(#)f is_bounded_on Y by A1,Th44; hence thesis by Th23; end; theorem Th46: f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y) proof assume that A1: f1 is_bounded_on X and A2: f2 is_bounded_on Y; consider r1 be Real such that A3: for c be Element of M st c in X /\ dom f1 holds ||.(f1/.c).|| <= r1 by A1; consider r2 be Real such that A4: for c be Element of M st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2 by A2; take r=r1+r2; let c be Element of M; assume A5: c in X /\ Y /\ dom (f1+f2); then A6: c in X /\ Y by XBOOLE_0:def 4; then A7: c in Y by XBOOLE_0:def 4; A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4; then A9: c in dom f1 /\ dom f2 by VFUNCT_1:def 1; then c in dom f2 by XBOOLE_0:def 4; then c in Y /\ dom f2 by A7,XBOOLE_0:def 4; then A10: ||.(f2/.c).|| <= r2 by A4; A11: c in X by A6,XBOOLE_0:def 4; c in dom f1 by A9,XBOOLE_0:def 4; then c in X /\ dom f1 by A11,XBOOLE_0:def 4; then ||.(f1/.c).|| <= r1 by A3; then ||.(f1/.c) + (f2/.c).|| <= ||.(f1/.c).|| + ||.f2/.c.|| & ||.(f1/.c).|| + ||. (f2/.c).|| <= r by A10,CLVECT_1:def 13,XREAL_1:7; then ||.(f1/.c) + (f2/.c).|| <= r by XXREAL_0:2; hence thesis by A8,VFUNCT_1:def 1; end; theorem for f1 be PartFunc of M,COMPLEX holds f1|X is bounded & f2 is_bounded_on Y implies f1(#)f2 is_bounded_on (X /\ Y) proof let f1 be PartFunc of M,COMPLEX; assume that A1: f1|X is bounded and A2: f2 is_bounded_on Y; consider r1 be Real such that A3: for c be Element of M st c in X /\ dom f1 holds |. f1/.c .| <= r1 by A1, CFUNCT_1:69; consider r2 be Real such that A4: for c be Element of M st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2 by A2; reconsider r1 as Real; now take r=r1*r2; let c be Element of M; assume A5: c in X /\ Y /\ dom (f1(#)f2); then A6: c in X /\ Y by XBOOLE_0:def 4; then A7: c in X by XBOOLE_0:def 4; A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4; then A9: c in dom f1 /\ dom f2 by Def1; then c in dom f1 by XBOOLE_0:def 4; then c in X /\ dom f1 by A7,XBOOLE_0:def 4; then A10: |.(f1/.c).| <= r1 by A3; A11: c in Y by A6,XBOOLE_0:def 4; c in dom f2 by A9,XBOOLE_0:def 4; then c in Y /\ dom f2 by A11,XBOOLE_0:def 4; then A12: ||.(f2/.c).|| <= r2 by A4; 0<=|.(f1/.c).| & 0<=||.(f2/.c).|| by CLVECT_1:105,COMPLEX1:46; then |.(f1/.c).|*||.(f2/.c).|| <= r by A10,A12,XREAL_1:66; then ||.f1/.c * (f2/.c).|| <= r by CLVECT_1:def 13; hence ||.(f1(#)f2)/.c.|| <= r by A8,Def1; end; hence thesis; end; theorem f1 is_bounded_on X & f2 is_bounded_on Y implies f1-f2 is_bounded_on X /\ Y proof assume that A1: f1 is_bounded_on X and A2: f2 is_bounded_on Y; -f2 is_bounded_on Y by A2,Th45; then f1+-f2 is_bounded_on (X /\ Y) by A1,Th46; hence thesis by Th25; end; theorem f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y proof assume that A1: f is_bounded_on X and A2: f is_bounded_on Y; consider r1 be Real such that A3: for c be Element of M st c in X /\ dom f holds ||.f/.c.|| <= r1 by A1; consider r2 be Real such that A4: for c be Element of M st c in Y /\ dom f holds ||.f/.c.|| <= r2 by A2; reconsider r = |.r1.| + |.r2.| as Real; take r; let c be Element of M; assume A5: c in (X \/ Y) /\ dom f; then A6: c in dom f by XBOOLE_0:def 4; A7: c in X \/ Y by A5,XBOOLE_0:def 4; now per cases by A7,XBOOLE_0:def 3; suppose c in X; then c in X /\ dom f by A6,XBOOLE_0:def 4; then A8: ||.f/.c.|| <= r1 by A3; A9: 0 <= |.r2.| by COMPLEX1:46; r1 <= |.r1.| by ABSVALUE:4; then ||.f/.c.|| <= |.r1.| by A8,XXREAL_0:2; then ||.f/.c.|| + 0 <= r by A9,XREAL_1:7; hence thesis; end; suppose c in Y; then c in Y /\ dom f by A6,XBOOLE_0:def 4; then A10: ||.f/.c.|| <= r2 by A4; A11: 0 <= |.r1.| by COMPLEX1:46; r2 <= |.r2.| by ABSVALUE:4; then ||.f/.c.|| <= |.r2.| by A10,XXREAL_0:2; then 0 + ||.f/.c.|| <= r by A11,XREAL_1:7; hence thesis; end; end; hence thesis; end; theorem f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is constant & (f1-f2)|(X /\ Y) is constant proof assume that A1: f1|X is constant and A2: f2|Y is constant; consider r1 being VECTOR of V such that A3: for c be Element of M st c in X /\ dom f1 holds (f1/.c) = r1 by A1, PARTFUN2:35; consider r2 being VECTOR of V such that A4: for c be Element of M st c in Y /\ dom f2 holds (f2/.c) = r2 by A2, PARTFUN2:35; now let c be Element of M; assume A5: c in X /\ Y /\ dom (f1+f2); then A6: c in X /\ Y by XBOOLE_0:def 4; then A7: c in X by XBOOLE_0:def 4; A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4; then A9: c in (dom f1 /\ dom f2) by VFUNCT_1:def 1; then c in dom f1 by XBOOLE_0:def 4; then A10: c in X /\ dom f1 by A7,XBOOLE_0:def 4; A11: c in Y by A6,XBOOLE_0:def 4; c in dom f2 by A9,XBOOLE_0:def 4; then A12: c in Y /\ dom f2 by A11,XBOOLE_0:def 4; thus (f1+f2)/.c = (f1/.c) + (f2/.c) by A8,VFUNCT_1:def 1 .= r1 + (f2/.c) by A3,A10 .= r1 + r2 by A4,A12; end; hence (f1+f2)|(X /\ Y) is constant by PARTFUN2:35; now let c be Element of M; assume A13: c in X /\ Y /\ dom (f1-f2); then A14: c in X /\ Y by XBOOLE_0:def 4; then A15: c in X by XBOOLE_0:def 4; A16: c in dom (f1-f2) by A13,XBOOLE_0:def 4; then A17: c in (dom f1 /\ dom f2) by VFUNCT_1:def 2; then c in dom f1 by XBOOLE_0:def 4; then A18: c in X /\ dom f1 by A15,XBOOLE_0:def 4; A19: c in Y by A14,XBOOLE_0:def 4; c in dom f2 by A17,XBOOLE_0:def 4; then A20: c in Y /\ dom f2 by A19,XBOOLE_0:def 4; thus (f1-f2)/.c = (f1/.c) - (f2/.c) by A16,VFUNCT_1:def 2 .= r1 - (f2/.c) by A3,A18 .= r1 - r2 by A4,A20; end; hence thesis by PARTFUN2:35; end; theorem for f1 be PartFunc of M,COMPLEX holds f1|X is constant & f2|Y is constant implies (f1(#)f2)|(X /\ Y) is constant proof let f1 be PartFunc of M,COMPLEX; assume that A1: f1|X is constant and A2: f2|Y is constant; consider z1 be Element of COMPLEX such that A3: for c be Element of M st c in X /\ dom f1 holds f1.c = z1 by A1,PARTFUN2:57; consider r2 being VECTOR of V such that A4: for c be Element of M st c in Y /\ dom f2 holds (f2/.c) = r2 by A2, PARTFUN2:35; now let c be Element of M; assume A5: c in X /\ Y /\ dom (f1(#)f2); then A6: c in X /\ Y by XBOOLE_0:def 4; then A7: c in Y by XBOOLE_0:def 4; A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4; then A9: c in (dom f1 /\ dom f2) by Def1; then A10: c in dom f1 by XBOOLE_0:def 4; then A11: f1/.c = f1.c by PARTFUN1:def 6; c in dom f2 by A9,XBOOLE_0:def 4; then A12: c in Y /\ dom f2 by A7,XBOOLE_0:def 4; c in X by A6,XBOOLE_0:def 4; then A13: c in X /\ dom f1 by A10,XBOOLE_0:def 4; thus (f1(#)f2)/.c = f1/.c * (f2/.c) by A8,Def1 .= z1 * (f2/.c) by A3,A13,A11 .= z1 * r2 by A4,A12; end; hence thesis by PARTFUN2:35; end; theorem Th52: f|Y is constant implies (z(#)f)|Y is constant proof assume f|Y is constant; then consider r being VECTOR of V such that A1: for c be Element of M st c in Y /\ dom f holds f/.c = r by PARTFUN2:35; now let c be Element of M; assume A2: c in Y /\ dom (z(#)f); then A3: c in Y by XBOOLE_0:def 4; A4: c in dom (z(#)f) by A2,XBOOLE_0:def 4; then c in dom f by Def2; then A5: c in Y /\ dom f by A3,XBOOLE_0:def 4; thus (z(#)f)/.c = z * f/.c by A4,Def2 .= z*r by A1,A5; end; hence thesis by PARTFUN2:35; end; theorem Th53: f|Y is constant implies ||.f.|||Y is constant & (-f)|Y is constant proof assume f|Y is constant; then consider r being VECTOR of V such that A1: for c be Element of M st c in Y /\ dom f holds f/.c = r by PARTFUN2:35; A2: ||.r.|| in REAL by XREAL_0:def 1; now let c be Element of M; assume A3: c in Y /\ dom (||.f.||); 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 A6: c in Y /\ dom f by A4,XBOOLE_0:def 4; thus (||.f.||).c = ||.f/.c.|| by A5,NORMSP_0:def 3 .= ||.r.|| by A1,A6; end; hence ||.f.|||Y is constant by PARTFUN2:57,A2; now take p=-r; let c be Element of M; assume A7: c in Y /\ dom (-f); then c in Y /\ dom f by VFUNCT_1:def 5; then A8: -f/.c = p by A1; c in dom (-f) by A7,XBOOLE_0:def 4; hence (-f)/.c = p by A8,VFUNCT_1:def 5; end; hence thesis by PARTFUN2:35; end; theorem Th54: f|Y is constant implies f is_bounded_on Y proof assume f|Y is constant; then consider r being VECTOR of V such that A1: for c be Element of M st c in Y /\ dom f holds f/.c = r by PARTFUN2:35; now reconsider p=||.r.|| as Real; take p; let c be Element of M; assume c in Y /\ dom f; hence ||.f/.c.|| <= p by A1; end; hence thesis; end; theorem f|Y is constant implies (for z holds z(#)f is_bounded_on Y) & -f is_bounded_on Y & ||.f.|||Y is bounded proof assume A1: f|Y is constant; hereby let z; (z(#)f)|Y is constant by A1,Th52; hence z(#)f is_bounded_on Y by Th54; end; (-f)|Y is constant by A1,Th53; hence -f is_bounded_on Y by Th54; ||.f.|||Y is constant by A1,Th53; hence thesis; end; theorem f1 is_bounded_on X & f2|Y is constant implies f1+f2 is_bounded_on (X /\ Y) proof assume that A1: f1 is_bounded_on X and A2: f2|Y is constant; f2 is_bounded_on Y by A2,Th54; hence thesis by A1,Th46; end; theorem f1 is_bounded_on X & f2|Y is constant implies f1-f2 is_bounded_on X /\ Y & f2-f1 is_bounded_on X /\ Y proof assume that A1: f1 is_bounded_on X and A2: f2|Y is constant; 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 thesis by A4,Th25; end;