### The Mizar article:

### Algebra of Vector Functions

**by****Hiroshi Yamazaki, and****Yasunari Shidama**

- Received October 27, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: VFUNCT_1
- [ MML identifier index ]

environ vocabulary NORMSP_1, PARTFUN1, RELAT_1, BOOLE, ARYTM_1, SEQ_1, FUNCT_1, RLVECT_1, ABSVALUE, RFUNCT_1, PARTFUN2, FINSEQ_4, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, STRUCT_0, ABSVALUE, FINSEQ_4, RELSET_1, PARTFUN1, PARTFUN2, RLVECT_1, NORMSP_1, SEQ_1, RFUNCT_1; constructors REAL_1, ABSVALUE, FINSEQ_4, PARTFUN1, PARTFUN2, NORMSP_1, RFUNCT_1, SEQ_1, MEMBERED, XBOOLE_0; clusters RELSET_1, STRUCT_0, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, PARTFUN1, XBOOLE_0; theorems TARSKI, AXIOMS, SUBSET_1, FUNCT_1, REAL_1, ABSVALUE, PARTFUN1, PARTFUN2, RFUNCT_1, RLVECT_1, NORMSP_1, SEQ_1, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1; schemes SEQ_1, PARTFUN2; begin reserve x,X,Y for set; reserve C for non empty set; reserve c for Element of C; reserve V for RealNormSpace; reserve f,f1,f2,f3 for PartFunc of C,the carrier of V; reserve r,r1,r2,p for Real; :: ::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS :: definition let C;let V;let f1,f2; deffunc F(Element of C) = (f1/.$1) + (f2/.$1); deffunc G(Element of C) = (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 C,the carrier of V means :Def1: dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = (f1/.c) + (f2/.c); existence proof consider F be PartFunc of C,the carrier of V such that A1: for c holds c in dom F iff P[c] and A2: for c st c in dom F holds F/.c = F(c) from LambdaPFD; take F; thus dom F = dom f1 /\ dom f2 by A1,SUBSET_1:8; let c; assume c in dom F; hence thesis by A2; end; uniqueness proof thus for f,g being PartFunc of C, the carrier of V st (dom f=X & for c be Element of C st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of C st c in dom g holds g/.c = F(c)) holds f = g from UnPartFuncD; end; func f1-f2 -> PartFunc of C,the carrier of V means :Def2: dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = (f1/.c) - (f2/.c); existence proof consider F be PartFunc of C,the carrier of V such that A3: for c holds c in dom F iff P[c] and A4: for c st c in dom F holds F/.c = G(c) from LambdaPFD; take F; thus dom F = dom f1 /\ dom f2 by A3,SUBSET_1:8; let c; assume c in dom F; hence thesis by A4; end; uniqueness proof thus for f,g being PartFunc of C, the carrier of V st (dom f=X & for c be Element of C st c in dom f holds f/.c = G(c)) & (dom g=X & for c be Element of C st c in dom g holds g/.c = G(c)) holds f = g from UnPartFuncD; end; end; definition let C;let V;let f1 be PartFunc of C,REAL;let f2; deffunc F(Element of C) = (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 C,the carrier of V means :Def3: dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = f1.c * (f2/.c); existence proof consider F be PartFunc of C,the carrier of V such that A1: for c holds c in dom F iff P[c] and A2: for c st c in dom F holds F/.c = F(c) from LambdaPFD; take F; thus dom F = dom f1 /\ dom f2 by A1,SUBSET_1:8; let c; assume c in dom F; hence thesis by A2; end; uniqueness proof thus for f,g being PartFunc of C, the carrier of V st (dom f=X & for c be Element of C st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of C st c in dom g holds g/.c = F(c)) holds f = g from UnPartFuncD; end; end; definition let C;let V;let f,r; deffunc F(Element of C) = r * (f/.$1); defpred P[set] means $1 in dom f; set X = dom f; func r(#)f -> PartFunc of C,the carrier of V means :Def4: dom it = dom f & for c st c in dom it holds it/.c = r * (f/.c); existence proof consider F be PartFunc of C,the carrier of V such that A1: for c holds c in dom F iff P[c] and A2: for c st c in dom F holds F/.c = F(c) from LambdaPFD; take F; thus dom F = dom f by A1,SUBSET_1:8; let c; assume c in dom F; hence thesis by A2; end; uniqueness proof thus for f,g being PartFunc of C, the carrier of V st (dom f=X & for c be Element of C st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of C st c in dom g holds g/.c = F(c)) holds f = g from UnPartFuncD; end; end; definition let C;let V; let f; deffunc F(Element of C) = ||. f/.$1 .||; deffunc G(Element of C) = - f/.$1; defpred P[set] means $1 in dom f; set X = dom f; func ||.f.|| -> PartFunc of C,REAL means :Def5: dom it = dom f & for c st c in dom it holds it.c = ||. f/.c .||; existence proof consider F be PartFunc of C,REAL such that A1: for c holds c in dom F iff P[c] and A2: for c st c in dom F holds F.c = F(c) from LambdaPFD'; take F; thus dom F = dom f by A1,SUBSET_1:8; let c; assume c in dom F; hence thesis by A2; end; uniqueness proof thus for h,g being PartFunc of C, REAL st (dom h=X & for c be Element of C st c in dom h holds h.c = F(c)) & (dom g=X & for c be Element of C st c in dom g holds g.c = F(c)) holds h = g from UnPartFuncD'; end; func -f ->PartFunc of C,the carrier of V means :Def6: dom it = dom f & for c st c in dom it holds it/.c = -(f/.c); existence proof consider F being PartFunc of C,the carrier of V such that A3: for c holds c in dom F iff P[c] and A4: for c st c in dom F holds F/.c = G(c) from LambdaPFD; take F; thus dom f = dom F by A3,SUBSET_1:8; let c; assume c in dom F; hence thesis by A4; end; uniqueness proof thus for f,g being PartFunc of C, the carrier of V st (dom f=X & for c be Element of C st c in dom f holds f/.c = G(c)) & (dom g=X & for c be Element of C st c in dom g holds g/.c = G(c)) holds f = g from UnPartFuncD; end; end; canceled 6; theorem for f1 be PartFunc of C,REAL holds dom (f1(#)f2) \ (f1(#)f2)"{0.V} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) proof let f1 be PartFunc of C,REAL; thus dom (f1(#)f2) \ (f1(#) f2)"{0.V} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) proof let x; assume A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0.V}; then A2: x in dom (f1(#)f2) & not x in (f1(#)f2)"{0.V} by XBOOLE_0:def 4; reconsider x1=x as Element of C by A1; not (f1(#)f2)/.x1 in {0.V} by A2,PARTFUN2:44; then (f1(#)f2)/.x1 <> 0.V by TARSKI:def 1; then f1.x1 * (f2/.x1) <> 0.V by A2,Def3; then f1.x1 <> 0 & (f2/.x1) <> 0.V by RLVECT_1:23; then x1 in dom f1 /\ dom f2 & not f1.x1 in {0} & not (f2/.x1) in {0.V} by A2,Def3,TARSKI:def 1; then x1 in dom f1 & x1 in dom f2 & not x1 in (f1)"{0} & not (f2/.x1) in {0.V } by FUNCT_1:def 13,XBOOLE_0:def 3; then x in dom f1 \ (f1)"{0} & x1 in dom f2 & not x1 in (f2)"{0.V} by PARTFUN2 :44,XBOOLE_0:def 4; then x in dom f1 \ (f1)"{0} & x in dom f2 \ (f2)"{0.V} by XBOOLE_0:def 4; hence x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) by XBOOLE_0:def 3; end; thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) c= dom (f1(#)f2) \ (f1(#) f2)"{0.V} proof let x; assume A3: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}); then x in dom f1 \ (f1)"{0} & x in dom f2 \ (f2)"{0.V} by XBOOLE_0:def 3; then A4: x in dom f1 & not x in (f1)"{0} & x in dom f2 & not x in (f2)"{0.V} by XBOOLE_0:def 4; reconsider x1=x as Element of C by A3; not f1.x1 in {0} by A4,FUNCT_1:def 13; then A5: f1.x1 <> 0 by TARSKI:def 1; not (f2/.x1) in {0.V} by A4,PARTFUN2:44; then (f2/.x1) <> 0.V by TARSKI:def 1; then A6: f1.x1 * (f2/.x1) <>0.V by A5,RLVECT_1:24; x1 in dom f1 /\ dom f2 by A4,XBOOLE_0:def 3; then A7: x1 in dom (f1(#)f2) by Def3; then (f1(#)f2)/.x1 <> 0.V by A6,Def3; then not (f1(#)f2)/.x1 in {0.V} by TARSKI:def 1; then not x in (f1(#)f2)"{0.V} by PARTFUN2:44; hence x in dom (f1(#)f2) \ (f1(#)f2)"{0.V} by A7,XBOOLE_0:def 4; end; end; theorem (||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V} proof now let c; thus c in (||.f.||)"{0} implies c in f"{0.V} proof assume c in (||.f.||)"{0}; then c in dom (||.f.||) & (||.f.||).c in {0} by FUNCT_1:def 13; then c in dom (||.f.||) & (||.f.||).c = 0 by TARSKI:def 1; then c in dom (||.f.||) & ||.f/.c.|| = 0 by Def5; then c in dom f & f/.c = 0.V by Def5,NORMSP_1:def 2; then c in dom f & f/.c in {0.V} by TARSKI:def 1; hence thesis by PARTFUN2:44; end; assume c in (f)"{0.V}; then c in dom f & f/.c in {0.V} by PARTFUN2:44; then c in dom (||.f.||) & f/.c = 0.V by Def5,TARSKI:def 1; then c in dom (||.f.||) & ||.f/.c.|| = 0 by NORMSP_1:def 2; then c in dom (||.f.||) & (||.f.||).c = 0 by Def5; then c in dom (||.f.||) & (||.f.||).c in {0} by TARSKI:def 1; hence c in (||.f.||)"{0} by FUNCT_1:def 13; end; hence (||.f.||)"{0} = f"{0.V} by SUBSET_1:8; now let c; thus c in (-f)"{0.V} implies c in f"{0.V} proof assume c in (-f)"{0.V}; then c in dom (-f) & (-f)/.c in {0.V} by PARTFUN2:44; then c in dom (-f) & (-f)/.c = 0.V by TARSKI:def 1; then c in dom (-f) & --(f/.c) = -0.V by Def6; then c in dom (-f) & --(f/.c) = 0.V by RLVECT_1:25; then c in dom f & f/.c = 0.V by Def6,RLVECT_1:30; then c in dom f & f/.c in {0.V} by TARSKI:def 1; hence thesis by PARTFUN2:44; end; assume c in (f)"{0.V}; then c in dom f & f/.c in {0.V} by PARTFUN2:44; then c in dom (-f) & f/.c = 0.V by Def6,TARSKI:def 1; then c in dom (-f) & (-f)/.c = -0.V by Def6; then c in dom (-f) & (-f)/.c = 0.V by RLVECT_1:25; then c in dom (-f) & (-f)/.c in {0.V} by TARSKI:def 1; hence c in (-f)"{0.V} by PARTFUN2:44; end; hence thesis by SUBSET_1:8; end; theorem r<>0 implies (r(#)f)"{0.V} = f"{0.V} proof assume A1: r<>0; now let c; thus c in (r(#)f)"{0.V} implies c in f"{0.V} proof assume c in (r(#)f)"{0.V}; then c in dom (r(#)f) & (r(#)f)/.c in {0.V} by PARTFUN2:44; then c in dom (r(#)f) & (r(#)f)/.c = 0.V by TARSKI:def 1; then c in dom f & r*f/.c = 0.V by Def4; then c in dom f & r*f/.c = r*0.V by RLVECT_1:23; then c in dom f & f/.c = 0.V by A1,RLVECT_1:50; then c in dom f & f/.c in {0.V} by TARSKI:def 1; hence thesis by PARTFUN2:44; end; assume c in (f)"{0.V}; then c in dom f & f/.c in {0.V} by PARTFUN2:44; then c in dom (r(#)f) & r*f/.c = r*0.V by Def4,TARSKI:def 1; then c in dom (r(#)f) & r*f/.c = 0.V by RLVECT_1:23; then c in dom (r(#)f) & (r(#)f)/.c = 0.V by Def4; then c in dom (r(#)f) & (r(#)f)/.c in {0.V} by TARSKI:def 1; hence c in (r(#)f)"{0.V} by PARTFUN2:44; end; hence thesis by SUBSET_1:8; end; :: :: BASIC PROPERTIES OF OPERATIONS :: theorem f1 + f2 = f2 + f1 proof A1: dom (f1 + f2) = dom f2 /\ dom f1 by Def1 .= dom (f2 + f1) by Def1; now let c; assume A2: c in dom (f1+f2); hence (f1 + f2)/.c = (f2/.c) + (f1/.c) by Def1 .= (f2 + f1)/.c by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:3; end; theorem (f1 + f2) + f3 = f1 + (f2 + f3) proof 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 let c; assume A2: c in dom (f1 + f2 + f3); then c in dom f1 /\ dom (f2 + f3) by A1,Def1; then A3: c in dom (f2 + f3) by XBOOLE_0:def 3; c in dom (f1 + f2) /\ dom f3 by A2,Def1; then A4: c in dom (f1 + f2) by XBOOLE_0:def 3; thus (f1 + f2 + f3)/.c = ((f1 + f2)/.c) + (f3/.c) by A2,Def1 .= (f1/.c) + (f2/.c) + (f3/.c) by A4,Def1 .= (f1/.c) + ((f2/.c) + (f3/.c)) by RLVECT_1:def 6 .= (f1/.c) + ((f2 + f3)/.c) by A3,Def1 .= (f1 + (f2 + f3))/.c by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:3; end; theorem for f1,f2 be PartFunc of C,REAL,f3 be PartFunc of C,the carrier of V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) proof let f1,f2 be PartFunc of C,REAL; let f3 be PartFunc of C,the carrier of V; A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by Def3 .= dom f1 /\ dom f2 /\ dom f3 by SEQ_1:def 5 .= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16 .= dom f1 /\ dom (f2 (#) f3) by Def3 .= dom (f1 (#) (f2 (#) f3)) by Def3; now let c; assume A2: c in dom (f1(#)f2(#)f3); then c in dom f1 /\ dom (f2(#)f3) by A1,Def3; then A3: c in dom (f2 (#) f3) by XBOOLE_0:def 3; c in dom (f1 (#) f2) /\ dom f3 by A2,Def3; then A4: c in dom (f1 (#) f2) by XBOOLE_0:def 3; thus (f1 (#) f2 (#) f3)/.c = (f1 (#) f2).c * (f3/.c) by A2,Def3 .= f1.c * f2.c * (f3/.c) by A4,SEQ_1:def 5 .= f1.c * (f2.c * (f3/.c)) by RLVECT_1:def 9 .= f1.c * ((f2 (#) f3)/.c) by A3,Def3 .= (f1 (#) (f2 (#) f3))/.c by A1,A2,Def3; end; hence thesis by A1,PARTFUN2:3; end; theorem for f1,f2 be PartFunc of C,REAL holds (f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3 proof let f1,f2 be PartFunc of C,REAL; A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by Def3 .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by SEQ_1:def 3 .= 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 let c; assume A2: c in dom ((f1 + f2)(#)f3); then c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,Def1; then A3: c in dom (f1(#)f3) & c in dom (f2 (#) f3) by XBOOLE_0:def 3; c in dom (f1 + f2) /\ dom f3 by A2,Def3; then A4: c in dom (f1 + f2) by XBOOLE_0:def 3; thus ((f1 + f2) (#) f3)/.c = (f1 + f2).c * (f3/.c) by A2,Def3 .= (f1.c + f2.c) * (f3/.c) by A4,SEQ_1:def 3 .= f1.c * (f3/.c) + f2.c * (f3/.c) by RLVECT_1:def 9 .= ((f1 (#) f3)/.c) + f2.c* (f3/.c) by A3,Def3 .= ((f1 (#) f3)/.c) + ((f2 (#) f3)/.c) by A3,Def3 .= ((f1 (#) f3) + (f2 (#) f3))/.c by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:3; end; theorem for f3 be PartFunc of C,REAL holds f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2 proof let f3 be PartFunc of C,REAL; 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 let c; assume A2: c in dom (f3(#)(f1 + f2)); then c in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,Def1; then A3: c in dom (f3(#)f1) & c in dom (f3 (#) f2) by XBOOLE_0:def 3; c in dom f3 /\ dom (f1 + f2) by A2,Def3; then A4: c in dom (f1 + f2) by XBOOLE_0:def 3; thus (f3 (#) (f1 + f2))/.c = f3.c * ((f1 + f2)/.c) by A2,Def3 .= f3.c * ((f1/.c) + (f2/.c)) by A4,Def1 .= f3.c * (f1/.c) + f3.c * (f2/.c) by RLVECT_1:def 9 .= ((f3 (#) f1)/.c) + f3.c* (f2/.c) by A3,Def3 .= ((f3 (#) f1)/.c) + ((f3 (#) f2)/.c) by A3,Def3 .= ((f3 (#) f1) + (f3 (#) f2))/.c by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:3; end; theorem for f1 be PartFunc of C,REAL holds r(#)(f1(#)f2)=r(#)f1(#)f2 proof let f1 be PartFunc of C,REAL; A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def4 .= dom f1 /\ dom f2 by Def3 .= dom (r(#)f1) /\ dom f2 by SEQ_1:def 6 .= dom (r(#)f1(#)f2) by Def3; now let c; assume A2: c in dom (r(#)(f1(#)f2)); then c in dom (r(#)f1) /\ dom f2 by A1,Def3; then A3: c in dom (r(#)f1) & c in dom f2 by XBOOLE_0:def 3; A4: c in dom (f1(#)f2) by A2,Def4; thus (r(#)(f1(#)f2))/.c = r * ((f1(#)f2)/.c) by A2,Def4 .= r*(f1.c * (f2/.c)) by A4,Def3 .= (r*f1.c) * (f2/.c) by RLVECT_1:def 9 .= (r(#)f1).c * (f2/.c) by A3,SEQ_1:def 6 .= (r(#)f1 (#) f2)/.c by A1,A2,Def3; end; hence thesis by A1,PARTFUN2:3; end; theorem for f1 be PartFunc of C,REAL holds r(#)(f1(#)f2)=f1(#)(r(#)f2) proof let f1 be PartFunc of C,REAL; 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 let c; assume A2: c in dom (r(#)(f1(#)f2)); then c in dom f1 /\ dom (r(#)f2) by A1,Def3; then A3: c in dom f1 & c in dom (r(#)f2) by XBOOLE_0:def 3; A4: c in dom (f1(#)f2) by A2,Def4; thus (r(#)(f1(#)f2))/.c = r * (f1(#)f2)/.c by A2,Def4 .= r * (f1.c * (f2/.c)) by A4,Def3 .= f1.c * r * (f2/.c) by RLVECT_1:def 9 .= f1.c * (r * (f2/.c)) by RLVECT_1:def 9 .= f1.c * ((r(#)f2)/.c) by A3,Def4 .= (f1(#)(r(#)f2))/.c by A1,A2,Def3; end; hence thesis by A1,PARTFUN2:3; end; theorem for f1,f2 be PartFunc of C,REAL holds (f1 - f2)(#)f3=f1(#)f3 - f2(#)f3 proof let f1,f2 be PartFunc of C,REAL; A1: dom ((f1 - f2) (#) f3) = dom (f1 - f2) /\ dom f3 by Def3 .= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by SEQ_1:def 4 .= 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 let c; assume A2: c in dom ((f1 - f2)(#)f3); then c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,Def2; then A3: c in dom (f1(#)f3) & c in dom (f2 (#) f3) by XBOOLE_0:def 3; c in dom (f1 - f2) /\ dom f3 by A2,Def3; then A4: c in dom (f1 - f2) by XBOOLE_0:def 3; thus ((f1 - f2) (#) f3)/.c = (f1 - f2).c * (f3/.c) by A2,Def3 .= (f1.c - f2.c) * (f3/.c) by A4,SEQ_1:def 4 .= f1.c * (f3/.c) - f2.c * (f3/.c) by RLVECT_1:49 .= ((f1 (#) f3)/.c) - f2.c * (f3/.c) by A3,Def3 .= ((f1 (#) f3)/.c) - ((f2 (#) f3)/.c) by A3,Def3 .= ((f1 (#) f3) - (f2 (#) f3))/.c by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:3; end; theorem for f3 be PartFunc of C,REAL holds f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) proof let f3 be PartFunc of C,REAL; 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 let c; assume A2: c in dom (f3(#)(f1 - f2)); then c in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,Def2; then A3: c in dom (f3(#)f1) & c in dom (f3 (#) f2) by XBOOLE_0:def 3; c in dom f3 /\ dom (f1 - f2) by A2,Def3; then A4: c in dom (f1 - f2) by XBOOLE_0:def 3; thus (f3 (#) (f1 - f2))/.c = f3.c * ((f1 - f2)/.c) by A2,Def3 .= f3.c * ((f1/.c) - (f2/.c)) by A4,Def2 .= f3.c * (f1/.c) - f3.c * (f2/.c) by RLVECT_1:48 .= ((f3 (#) f1)/.c) - f3.c * (f2/.c) by A3,Def3 .= ((f3 (#) f1)/.c) - ((f3 (#) f2)/.c) by A3,Def3 .= ((f3 (#) f1) - (f3 (#) f2))/.c by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:3; end; theorem r(#)(f1 + f2) = r(#)f1 + r(#)f2 proof 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 let c; assume A2: c in dom (r(#)(f1 + f2)); then c in dom (r(#)f1) /\ dom (r(#)f2) by A1,Def1; then A3: c in dom (r(#)f1) & c in dom (r(#)f2) by XBOOLE_0:def 3; A4: c in dom (f1 + f2) by A2,Def4; thus (r(#)(f1 + f2))/.c = r * ((f1 + f2)/.c) by A2,Def4 .= r * ((f1/.c) + (f2/.c)) by A4,Def1 .= r * (f1/.c) + r * (f2/.c) by RLVECT_1:def 9 .= ((r(#)f1)/.c) + r * (f2/.c) by A3,Def4 .= ((r(#)f1)/.c) + ((r(#)f2)/.c) by A3,Def4 .= (r(#)f1 + r(#)f2)/.c by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:3; end; theorem Th20: (r*p)(#)f = r(#)(p(#)f) proof A1: dom ((r*p) (#) f) = dom f by Def4 .= dom (p(#)f) by Def4 .= dom (r(#)(p(#)f)) by Def4; now let c; assume A2: c in dom ((r*p)(#)f); 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 9 .= r * ((p(#)f)/.c) by A3,Def4 .= (r(#)(p(#)f))/.c by A1,A2,Def4; end; hence thesis by A1,PARTFUN2:3; end; theorem r(#)(f1 - f2) = r(#)f1 - r(#)f2 proof 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 let c; assume A2: c in dom (r(#)(f1 - f2)); then c in dom (r(#)f1) /\ dom (r(#)f2) by A1,Def2; then A3: c in dom (r(#)f1) & c in dom (r(#)f2) by XBOOLE_0:def 3; A4: c in dom (f1 - f2) by A2,Def4; thus (r(#)(f1 - f2))/.c = r * ((f1 - f2)/.c) by A2,Def4 .= r * ((f1/.c) - (f2/.c)) by A4,Def2 .= r * (f1/.c) - r * (f2/.c) by RLVECT_1:48 .= ((r(#)f1)/.c) - r * (f2/.c) by A3,Def4 .= ((r(#)f1)/.c) - ((r(#)f2)/.c) by A3,Def4 .= (r(#)f1 - r(#)f2)/.c by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:3; end; theorem f1-f2 = (-1)(#)(f2-f1) proof A1: dom (f1 - f2) = dom f2 /\ dom f1 by Def2 .= dom (f2 - f1) by Def2 .= dom ((-1)(#)(f2 - f1)) by Def4; now let c such that A2: c in dom (f1-f2); A3: dom (f1 - f2) = dom f2 /\ dom f1 by Def2 .= dom (f2 - f1) by Def2; thus (f1 - f2)/.c = (f1/.c) - (f2/.c) by A2,Def2 .= -(f2/.c) + (f1/.c) by RLVECT_1:def 11 .= -((f2/.c) - (f1/.c)) by RLVECT_1:47 .= (-1)*((f2/.c) - (f1/.c)) by RLVECT_1:29 .= (-1)*((f2 - f1)/.c) by A2,A3,Def2 .= ((-1)(#)(f2 - f1))/.c by A1,A2,Def4; end; hence thesis by A1,PARTFUN2:3; end; theorem f1 - (f2 + f3) = f1 - f2 - f3 proof 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 let c; assume A2: c in dom (f1 - (f2 + f3)); then c in dom (f1 - f2) /\ dom f3 by A1,Def2; then A3: c in dom (f1 - f2) by XBOOLE_0:def 3; c in dom f1 /\ dom (f2 + f3) by A2,Def2; then A4: c in dom (f2 + f3) by XBOOLE_0:def 3; thus (f1 - (f2 + f3))/.c = (f1/.c) - ((f2 + f3)/.c) by A2,Def2 .= (f1/.c) - ((f2/.c) + (f3/.c)) by A4,Def1 .= (f1/.c) - (f2/.c) - (f3/.c) by RLVECT_1:41 .= ((f1 - f2)/.c) - (f3/.c) by A3,Def2 .= (f1 - f2 - f3)/.c by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:3; end; theorem Th24: 1(#)f = f proof A1: dom (1(#)f) = dom f by Def4; now let c; assume c in dom (1(#)f); hence (1(#)f)/.c = 1 * f/.c by Def4 .= f/.c by RLVECT_1:def 9; end; hence thesis by A1,PARTFUN2:3; end; theorem f1 - (f2 - f3) = f1 - f2 + f3 proof 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 let c; assume A2: c in dom (f1 - (f2 - f3)); then c in dom (f1 - f2) /\ dom f3 by A1,Def1; then A3: c in dom (f1 - f2) by XBOOLE_0:def 3; c in dom f1 /\ dom (f2 - f3) by A2,Def2; then A4: c in dom (f2 - f3) by XBOOLE_0:def 3; thus (f1 - (f2 - f3))/.c = (f1/.c) - ((f2 - f3)/.c) by A2,Def2 .= (f1/.c) - ((f2/.c) - (f3/.c)) by A4,Def2 .= (f1/.c) - (f2/.c) + (f3/.c) by RLVECT_1:43 .= ((f1 - f2)/.c) + (f3/.c) by A3,Def2 .= (f1 - f2 + f3)/.c by A1,A2,Def1; end; hence thesis by A1,PARTFUN2:3; end; theorem f1 + (f2 - f3) = f1 + f2 - f3 proof 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 let c; assume A2: c in dom (f1 + (f2 - f3)); then c in dom (f1 + f2) /\ dom f3 by A1,Def2; then A3: c in dom (f1 + f2) by XBOOLE_0:def 3; c in dom f1 /\ dom (f2 - f3) by A2,Def1; then A4: c in dom (f2 - f3) by XBOOLE_0:def 3; thus (f1 + (f2 - f3))/.c = (f1/.c) + ((f2 - f3)/.c) by A2,Def1 .= (f1/.c) + ((f2/.c) - (f3/.c)) by A4,Def2 .= (f1/.c) + (f2/.c) - (f3/.c) by RLVECT_1:42 .= ((f1 + f2)/.c) - (f3/.c) by A3,Def1 .= (f1 + f2 - f3)/.c by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:3; end; theorem for f1 be PartFunc of C,REAL holds ||.f1(#)f2.|| = abs(f1)(#)||.f2.|| proof let f1 be PartFunc of C,REAL; A1: dom (||.f1 (#) f2.||) = dom (f1 (#) f2) by Def5 .= dom f1 /\ dom f2 by Def3 .= dom f1 /\ dom (||.f2.||) by Def5 .= dom (abs(f1)) /\ dom (||.f2.||) by SEQ_1:def 10 .= dom (abs(f1)(#)||.f2.||) by SEQ_1:def 5; now let c; assume A2: c in dom (||.f1 (#) f2.||); then c in dom (abs(f1)) /\ dom (||.f2.||) by A1,SEQ_1:def 5; then A3: c in dom (abs(f1)) & c in dom (||.f2.||) by XBOOLE_0:def 3; A4: c in dom (f1 (#) f2) by A2,Def5; thus (||.f1(#)f2.||).c = ||.(f1(#)f2)/.c.|| by A2,Def5 .= ||.f1.c * (f2/.c).|| by A4,Def3 .= abs(f1.c) * ||.(f2/.c).|| by NORMSP_1:def 2 .= ((abs(f1)).c) * ||.(f2/.c).|| by A3,SEQ_1:def 10 .= ((abs(f1)).c) * (||.f2.||).c by A3,Def5 .= (abs(f1)(#)||.f2.||).c by A1,A2,SEQ_1:def 5; end; hence thesis by A1,PARTFUN1:34; end; theorem ||.r(#)f.|| = abs(r)(#)||.f.|| proof A1: dom (||.r(#)f.||) = dom (r(#)f) by Def5 .= dom f by Def4 .= dom (||.f.||) by Def5 .= dom (abs(r)(#)||.f.||) by SEQ_1:def 6; now let c; assume A2: c in dom (||.r(#)f.||); then A3: c in dom (||.f.||) by A1,SEQ_1:def 6; A4: c in dom (r(#)f) by A2,Def5; thus (||.r(#)f.||).c = ||.(r(#)f)/.c.|| by A2,Def5 .=||.r*(f/.c).|| by A4,Def4 .=abs(r)*||.f/.c.|| by NORMSP_1:def 2 .=abs(r)*(||.f.||.c) by A3,Def5 .=(abs(r)(#)||.f.||).c by A1,A2,SEQ_1:def 6; end; hence thesis by A1,PARTFUN1:34; end; theorem Th29: -f = (-1)(#)f proof A1: dom (-f) = dom f by Def6 .= dom ((-1)(#)f) by Def4; now let c; assume A2: c in dom ((-1)(#)f); hence (-f)/.c = -(f/.c) by A1,Def6 .= (-1) * f/.c by RLVECT_1:29 .= ((-1)(#)f)/.c by A2,Def4; end; hence thesis by A1,PARTFUN2:3; end; theorem Th30: -(-f) = f proof thus -(-f) = (-1)(#)(-f) by Th29 .= (-1)(#)((-1)(#)f) by Th29 .= ((-1)*(-1))(#)f by Th20 .= f by Th24; end; theorem Th31: f1 - f2 = f1 + -f2 proof A1: dom (f1 - f2) = dom f1 /\ dom f2 by Def2 .= dom f1 /\ dom (-f2) by Def6 .= dom (f1 + -f2) by Def1; now let c; assume A2: c in dom (f1+-f2); then c in dom f1 /\ dom (-f2) by Def1; then A3: c in dom (-f2) by XBOOLE_0:def 3; thus (f1 + -f2)/.c = (f1/.c) + ((-f2)/.c) by A2,Def1 .= (f1/.c) + -(f2/.c) by A3,Def6 .= (f1/.c) - (f2/.c) by RLVECT_1:def 11 .= (f1-f2)/.c by A1,A2,Def2; end; hence thesis by A1,PARTFUN2:3; end; theorem f1 - (-f2) = f1 + f2 proof thus f1 - (-f2) = f1 + (-(-f2)) by Th31 .= f1 + f2 by Th30; end; theorem Th33: (f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X proof A1: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90 .= 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:90 .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16 .= dom (f1|X) /\ dom (f2|X) by RELAT_1:90 .= dom ((f1|X)+(f2|X)) by Def1; now let c; assume A2: c in dom ((f1+f2)|X); then c in dom (f1+f2) /\ X by RELAT_1:90; then A3: c in dom (f1+f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by Def1; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f1|X) & c in dom (f2|X) by RELAT_1:90; then c in dom (f1|X) /\ dom (f2|X) by XBOOLE_0:def 3; then A5: c in dom ((f1|X) + (f2|X)) by Def1; thus ((f1+f2)|X)/.c = (f1+f2)/.c by A2,PARTFUN2:32 .= (f1/.c) + (f2/.c) by A3,Def1 .= ((f1|X)/.c) + (f2/.c) by A4,PARTFUN2:32 .= ((f1|X)/.c) + ((f2|X)/.c) by A4,PARTFUN2:32 .= ((f1|X)+(f2|X))/.c by A5,Def1; end; hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN2:3; A6: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by Def1 .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16 .= dom (f1|X) /\ dom f2 by RELAT_1:90 .= dom ((f1|X)+ f2) by Def1; now let c; assume A7: c in dom ((f1+f2)|X); then c in dom (f1+f2) /\ X by RELAT_1:90; then A8: c in dom (f1+f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by Def1; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 by A8,XBOOLE_0:def 3; then A9: c in dom (f1|X) & c in dom f2 by RELAT_1:90; then c in dom (f1|X) /\ dom f2 by XBOOLE_0:def 3; then A10: c in dom ((f1|X) + f2) by Def1; thus ((f1+f2)|X)/.c = (f1+f2)/.c by A7,PARTFUN2:32 .= (f1/.c) + (f2/.c) by A8,Def1 .= ((f1|X)/.c) +(f2/.c) by A9,PARTFUN2:32 .= ((f1|X)+f2)/.c by A10,Def1; end; hence (f1+f2)|X = f1|X + f2 by A6,PARTFUN2:3; A11: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by Def1 .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16 .= dom f1 /\ dom (f2|X) by RELAT_1:90 .= dom (f1 + (f2|X)) by Def1; now let c; assume A12: c in dom ((f1+f2)|X); then c in dom (f1+f2) /\ X by RELAT_1:90; then A13: c in dom (f1+f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by Def1; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 & c in dom f2 /\ X by A13,XBOOLE_0:def 3; then A14: c in dom f1 & c in dom (f2|X) by RELAT_1:90; then c in dom f1 /\ dom (f2|X) by XBOOLE_0:def 3; then A15: c in dom (f1 + (f2|X)) by Def1; thus ((f1+f2)|X)/.c = (f1+f2)/.c by A12,PARTFUN2:32 .= (f1/.c) +(f2/.c) by A13,Def1 .= (f1/.c) + ((f2|X)/.c) by A14,PARTFUN2:32 .= (f1+(f2|X))/.c by A15,Def1; end; hence thesis by A11,PARTFUN2:3; end; theorem for f1 be 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 f1 be PartFunc of C,REAL; A1: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90 .= 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:90 .= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16 .= dom (f1|X) /\ dom (f2|X) by RELAT_1:90 .= dom ((f1|X)(#)(f2|X)) by Def3; now let c; assume A2: c in dom ((f1(#)f2)|X); then c in dom (f1(#)f2) /\ X by RELAT_1:90; then A3: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by Def3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f1|X) & c in dom (f2|X) by RELAT_1:90; then c in dom (f1|X) /\ dom (f2|X) by XBOOLE_0:def 3; then A5: c in dom ((f1|X) (#) (f2|X)) by Def3; thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A2,PARTFUN2:32 .= (f1.c) * (f2/.c) by A3,Def3 .= ((f1|X).c) * (f2/.c) by A4,FUNCT_1:70 .= ((f1|X).c) * ((f2|X)/.c) by A4,PARTFUN2:32 .= ((f1|X)(#)(f2|X))/.c by A5,Def3; end; hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN2:3; A6: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by Def3 .= dom f1 /\ X /\ dom f2 by XBOOLE_1:16 .= dom (f1|X) /\ dom f2 by RELAT_1:90 .= dom ((f1|X)(#) f2) by Def3; now let c; assume A7: c in dom ((f1(#)f2)|X); then c in dom (f1(#)f2) /\ X by RELAT_1:90; then A8: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by Def3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 /\ X & c in dom f2 by A8,XBOOLE_0:def 3; then A9: c in dom (f1|X) & c in dom f2 by RELAT_1:90; then c in dom (f1|X) /\ dom f2 by XBOOLE_0:def 3; then A10: c in dom ((f1|X) (#) f2) by Def3; thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A7,PARTFUN2:32 .= (f1.c) * (f2/.c) by A8,Def3 .= ((f1|X).c) * (f2/.c) by A9,FUNCT_1:70 .= ((f1|X)(#)f2)/.c by A10,Def3; end; hence (f1(#)f2)|X = f1|X (#) f2 by A6,PARTFUN2:3; A11: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90 .= dom f1 /\ dom f2 /\ X by Def3 .= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16 .= dom f1 /\ dom (f2|X) by RELAT_1:90 .= dom (f1 (#) (f2|X)) by Def3; now let c; assume A12: c in dom ((f1(#)f2)|X); then c in dom (f1(#)f2) /\ X by RELAT_1:90; then A13: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3; then c in dom f1 /\ dom f2 by Def3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then c in dom f1 & c in dom f2 /\ X by A13,XBOOLE_0:def 3; then A14: c in dom f1 & c in dom (f2|X) by RELAT_1:90; then c in dom f1 /\ dom (f2|X) by XBOOLE_0:def 3; then A15: c in dom (f1 (#) (f2|X)) by Def3; thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A12,PARTFUN2:32 .= (f1.c) * (f2/.c) by A13,Def3 .= (f1.c) * ((f2|X)/.c) by A14,PARTFUN2:32 .= (f1(#)(f2|X))/.c by A15,Def3; end; hence thesis by A11,PARTFUN2:3; end; theorem Th35: (-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).|| proof A1: dom ((-f)|X) = dom (-f) /\ X by RELAT_1:90 .= dom f /\ X by Def6 .= dom (f|X) by RELAT_1:90 .= dom (-(f|X)) by Def6; now let c; assume A2: c in dom ((-f)|X); then c in dom (-f) /\ X by RELAT_1:90; then A3: c in dom (-f) & c in X by XBOOLE_0:def 3; then c in dom f by Def6; then c in dom f /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f|X) by RELAT_1:90; then A5: c in dom (-(f|X)) by Def6; thus ((-f)|X)/.c = (-f)/.c by A2,PARTFUN2:32 .= -(f/.c) by A3,Def6 .= -((f|X)/.c) by A4,PARTFUN2:32 .= (-(f|X))/.c by A5,Def6; end; hence (-f)|X = -(f|X) by A1,PARTFUN2:3; A6: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:90 .= dom f /\ X by Def5 .= dom (f|X) by RELAT_1:90 .= dom (||.(f|X).||) by Def5; now let c; assume A7: c in dom ((||.f.||)|X); then c in dom (||.f.||) /\ X by RELAT_1:90; then A8: c in dom (||.f.||) & c in X by XBOOLE_0:def 3; A9: c in dom (f|X) by A6,A7,Def5; thus ((||.f.||)|X).c = (||.f.||).c by A7,FUNCT_1:70 .= ||.f/.c.|| by A8,Def5 .= ||.(f|X)/.c.|| by A9,PARTFUN2:32 .= (||.(f|X).||).c by A6,A7,Def5; end; hence thesis by A6,PARTFUN1:34; 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 Th31 .= (f1|X)+ (-f2)|X by Th33 .= (f1|X)+ -(f2|X) by Th35 .= (f1|X) - (f2|X) by Th31; thus (f1-f2)|X = (f1+-f2)|X by Th31 .= (f1|X)+ -f2 by Th33 .= (f1|X) - f2 by Th31; thus (f1-f2)|X = (f1+-f2)|X by Th31 .= f1+ (-f2)|X by Th33 .= f1 +- (f2|X) by Th35 .= f1 - (f2|X) by Th31; end; theorem (r(#)f)|X = r(#)(f|X) proof A1: dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:90 .= dom f /\ X by Def4 .= dom (f|X) by RELAT_1:90 .= dom (r(#)(f|X)) by Def4; now let c; assume A2: c in dom ((r(#)f)|X); then c in dom (r(#)f) /\ X by RELAT_1:90; then A3: c in dom (r(#)f) & c in X by XBOOLE_0:def 3; then c in dom f by Def4; then c in dom f /\ X by A3,XBOOLE_0:def 3; then A4: c in dom (f|X) by RELAT_1:90; then A5: c in dom (r(#)(f|X)) by Def4; thus ((r(#)f)|X)/.c = (r(#)f)/.c by A2,PARTFUN2:32 .= r*(f/.c) by A3,Def4 .= r*((f|X)/.c) by A4,PARTFUN2:32 .= (r(#)(f|X))/.c by A5,Def4; end; hence thesis by A1,PARTFUN2:3; end; :: :: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO REAL :: theorem Th38: (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 = C & dom f2 = C by PARTFUN1:def 4; hence dom (f1+f2) = C /\ C by Def1 .= C; end; assume f1+f2 is total; then dom (f1+f2) = C by PARTFUN1:def 4; 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; 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 = C & dom f2 = C by PARTFUN1:def 4; hence dom (f1-f2) = C /\ C by Def2 .= C; end; assume f1-f2 is total; then dom (f1-f2) = C by PARTFUN1:def 4; 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; end; end; theorem Th39: for f1 be PartFunc of C,REAL holds (f1 is total & f2 is total iff f1(#)f2 is total) proof let f1 be PartFunc of C,REAL; thus f1 is total & f2 is total implies f1(#)f2 is total proof assume f1 is total & f2 is total; then dom f1 = C & dom f2 = C by PARTFUN1:def 4; hence dom (f1(#)f2) = C /\ C by Def3 .= C; end; assume f1(#)f2 is total; then dom (f1(#)f2) = C by PARTFUN1:def 4; 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; end; theorem Th40: f is total iff r(#)f is total proof thus f is total implies r(#)f is total proof assume f is total; then dom f = C by PARTFUN1:def 4; hence dom (r(#)f) = C by Def4; end; assume r(#)f is total; then dom (r(#)f) = C by PARTFUN1:def 4; hence dom f = C by Def4; end; theorem Th41: f is total iff -f is total proof thus f is total implies -f is total proof assume A1: f is total; -f = (-1)(#) f by Th29; hence -f is total by A1,Th40; end; assume A2: -f is total; -f = (-1)(#)f by Th29; hence f is total by A2,Th40; end; theorem Th42: f is total iff ||.f.|| is total proof thus f is total implies ||.f.|| is total proof assume f is total; then dom f = C by PARTFUN1:def 4; hence dom (||.f.||) = C by Def5; end; assume ||.f.|| is total; then dom (||.f.||) = C by PARTFUN1:def 4; hence dom f = C by Def5; end; theorem f1 is total & f2 is total implies (f1+f2)/.c = (f1/.c) + (f2/.c) & (f1-f2)/.c = (f1/.c) - (f2/.c) proof assume A1: f1 is total & f2 is total; then f1+f2 is total by Th38; then dom (f1+f2) = C by PARTFUN1:def 4; hence (f1+f2)/.c = (f1/.c) + (f2/.c) by Def1; f1-f2 is total by A1,Th38; then dom (f1-f2) = C by PARTFUN1:def 4; hence (f1-f2)/.c = (f1/.c) - (f2/.c) by Def2; end; theorem for f1 be PartFunc of C,REAL holds f1 is total & f2 is total implies (f1(#)f2)/.c = f1.c * (f2/.c) proof let f1 be PartFunc of C,REAL; assume f1 is total & f2 is total; then f1(#)f2 is total by Th39; then dom (f1(#)f2) = C by PARTFUN1:def 4; hence thesis by Def3; end; theorem f is total implies (r(#)f)/.c = r * (f/.c) proof assume f is total; then r(#)f is total by Th40; then dom (r(#)f) = C by PARTFUN1:def 4; hence thesis by Def4; end; theorem f is total implies (-f)/.c = - f/.c & (||.f.||).c = ||. f/.c .|| proof assume A1: f is total; then -f is total by Th41; then dom (-f) = C by PARTFUN1:def 4; hence (-f)/.c = - f/.c by Def6; ||.f.|| is total by A1,Th42; then dom (||.f.||) = C by PARTFUN1:def 4; hence thesis by Def5; end; :: :: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN TO A NORMED REAL SPACE :: definition let C; let V; let f,Y; pred f is_bounded_on Y means :Def7: ex r st for c st c in Y /\ dom f holds ||.f/.c.|| <= r; end; canceled; theorem Y c= X & f is_bounded_on X implies f is_bounded_on Y proof assume A1: Y c= X & f is_bounded_on X; then consider r such that A2: for c st c in X /\ dom f holds ||.f/.c.|| <= r by Def7; take r; let c; assume c in Y /\ dom f; then c in Y & c in dom f by XBOOLE_0:def 3; then c in X /\ dom f by A1,XBOOLE_0:def 3; hence thesis by A2; end; theorem X misses dom f implies f is_bounded_on X proof assume X /\ dom f = {}; then for c holds c in X /\ dom f implies ||.f/.c.|| <= 0; hence thesis by Def7; end; theorem 0(#)f is_bounded_on Y proof now take p=0; let c; assume c in Y /\ dom (0(#)f); then A1: c in dom (0(#)f) by XBOOLE_0:def 3; 0*||.f/.c.|| = 0; then abs(0)*||.f/.c.|| <= 0 by ABSVALUE:7; then ||.0*(f/.c).|| <= 0 by NORMSP_1:def 2; hence ||.(0(#)f)/.c.|| <= p by A1,Def4; end; hence thesis by Def7; end; theorem Th51: f is_bounded_on Y implies r(#)f is_bounded_on Y proof assume f is_bounded_on Y; then consider r1 such that A1: for c st c in Y /\ dom f holds ||.f/.c.|| <= r1 by Def7; take p = abs(r)*abs(r1); let c; assume c in Y /\ dom (r(#)f); then A2: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3; then c in Y & c in dom f by Def4; then c in Y /\ dom f by XBOOLE_0:def 3; then A3: ||.f/.c.|| <= r1 by A1; A4: abs(r) >= 0 by ABSVALUE:5; r1 <= abs(r1) by ABSVALUE:11; then ||.f/.c.|| <= abs(r1) by A3,AXIOMS:22; then abs(r) * ||.(f/.c).|| <= abs(r)*abs(r1) by A4,AXIOMS:25; then ||.r * (f/.c).|| <= p by NORMSP_1:def 2; hence ||.(r(#)f)/.c.|| <= p by A2,Def4; end; theorem Th52: f is_bounded_on Y implies ||.f.|| is_bounded_on Y & -f is_bounded_on Y proof assume A1: f is_bounded_on Y; then consider r1 such that A2: for c st c in Y /\ dom f holds ||.f/.c.|| <= r1 by Def7; now let c; A3: ||.f/.c.|| >= 0 by NORMSP_1:8; assume c in Y /\ dom (||.f.||); then A4: c in Y & c in dom (||.f.||) by XBOOLE_0:def 3; then c in dom f by Def5; then c in Y /\ dom f by A4,XBOOLE_0:def 3; then ||.f/.c.|| <= r1 by A2; then abs(||.f/.c.||) <= r1 by A3,ABSVALUE:def 1; hence abs((||.f.||).c) <= r1 by A4,Def5; end; hence ||.f.|| is_bounded_on Y by RFUNCT_1:90; (-1)(#)f is_bounded_on Y by A1,Th51; hence thesis by Th29; end; theorem Th53: f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y) proof assume A1: f1 is_bounded_on X & f2 is_bounded_on Y; then consider r1 such that A2: for c st c in X /\ dom f1 holds ||.(f1/.c).|| <= r1 by Def7; consider r2 such that A3: for c st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2 by A1,Def7; take r=r1+r2; let c; A4: ||.(f1/.c) + (f2/.c).|| <= ||.(f1/.c).|| + ||.f2/.c.|| by NORMSP_1:def 2; assume c in X /\ Y /\ dom (f1+f2); then A5: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3; then A6:c in X & c in Y & c in dom f1 /\ dom f2 by Def1,XBOOLE_0:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A7: c in X /\ dom f1 & c in Y /\ dom f2 by A6,XBOOLE_0:def 3; then A8: ||.(f1/.c).|| <= r1 by A2; ||.(f2/.c).|| <= r2 by A3,A7; then ||.(f1/.c).|| + ||.(f2/.c).|| <= r by A8,REAL_1:55; then ||.(f1/.c) + (f2/.c).|| <= r by A4,AXIOMS:22; hence ||.(f1+f2)/.c.|| <= r by A5,Def1; end; theorem for f1 be PartFunc of C,REAL holds f1 is_bounded_on X & f2 is_bounded_on Y implies f1(#)f2 is_bounded_on (X /\ Y) proof let f1 be PartFunc of C,REAL; assume A1: f1 is_bounded_on X & f2 is_bounded_on Y; then consider r1 be real number such that A2: for c st c in X /\ dom f1 holds abs(f1.c) <= r1 by RFUNCT_1:90; reconsider r1 as Real by XREAL_0:def 1; consider r2 such that A3: for c st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2 by A1,Def7; now take r=r1*r2; let c; assume c in X /\ Y /\ dom (f1(#)f2); then A4: c in X /\ Y & c in dom (f1(#)f2) by XBOOLE_0:def 3; then A5:c in X & c in Y & c in dom f1 /\ dom f2 by Def3,XBOOLE_0:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A6: c in X /\ dom f1 & c in Y /\ dom f2 by A5,XBOOLE_0:def 3; then A7: abs(f1.c) <= r1 by A2; A8: ||.(f2/.c).|| <= r2 by A3,A6; A9: 0<=abs(f1.c) by ABSVALUE:5; 0<=||.(f2/.c).|| by NORMSP_1:8; then abs(f1.c)*||.(f2/.c).|| <= r by A7,A8,A9,RFUNCT_1:2; then ||.f1.c * (f2/.c).|| <= r by NORMSP_1:def 2 ; hence ||.(f1(#)f2)/.c.|| <= r by A4,Def3; end; hence f1(#)f2 is_bounded_on X /\ Y by Def7; end; theorem f1 is_bounded_on X & f2 is_bounded_on Y implies f1-f2 is_bounded_on X /\ Y proof assume A1: f1 is_bounded_on X & f2 is_bounded_on Y; then -f2 is_bounded_on Y by Th52; then f1+-f2 is_bounded_on (X /\ Y) by A1,Th53; hence thesis by Th31; end; theorem f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y proof assume A1: f is_bounded_on X & f is_bounded_on Y; then consider r1 such that A2: for c st c in X /\ dom f holds ||.f/.c.|| <= r1 by Def7; consider r2 such that A3: for c st c in Y /\ dom f holds ||.f/.c.|| <= r2 by A1,Def7; take r = abs(r1) + abs(r2); let c; assume c in (X \/ Y) /\ dom f; then A4: c in X \/ Y & c in dom f by XBOOLE_0:def 3; now per cases by A4,XBOOLE_0:def 2; suppose c in X; then c in X /\ dom f by A4,XBOOLE_0:def 3; then A5: ||.f/.c.|| <= r1 by A2; r1 <= abs(r1) by ABSVALUE:11; then A6: ||.f/.c.|| <= abs(r1) by A5,AXIOMS:22; 0 <= abs(r2) by ABSVALUE:5; then ||.f/.c.|| + 0 <= r by A6,REAL_1:55; hence ||.f/.c.|| <= r; suppose c in Y; then c in Y /\ dom f by A4,XBOOLE_0:def 3; then A7: ||.f/.c.|| <= r2 by A3; r2 <= abs(r2) by ABSVALUE:11; then A8: ||.f/.c.|| <= abs(r2) by A7,AXIOMS:22; 0 <= abs(r1) by ABSVALUE:5; then 0 + ||.f/.c.|| <= r by A8,REAL_1:55; hence ||.f/.c.|| <= r; end; hence ||.f/.c.|| <= r; end; theorem f1 is_constant_on X & f2 is_constant_on Y implies (f1 + f2) is_constant_on (X /\ Y) & (f1 - f2) is_constant_on (X /\ Y) proof assume A1: f1 is_constant_on X & f2 is_constant_on Y; then consider r1 being VECTOR of V such that A2: for c st c in X /\ dom f1 holds (f1/.c) = r1 by PARTFUN2:def 3; consider r2 being VECTOR of V such that A3: for c st c in Y /\ dom f2 holds (f2/.c) = r2 by A1,PARTFUN2:def 3; now let c; assume c in X /\ Y /\ dom (f1+f2); then A4: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3; then A5: c in X & c in Y & c in (dom f1 /\ dom f2) by Def1,XBOOLE_0:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A6: c in X /\ dom f1 & c in Y /\ dom f2 by A5,XBOOLE_0:def 3; thus (f1+f2)/.c = (f1/.c) + (f2/.c) by A4,Def1 .= r1 + (f2/.c) by A2,A6 .= r1 + r2 by A3,A6; end; hence (f1 + f2) is_constant_on (X /\ Y) by PARTFUN2:def 3; now let c; assume c in X /\ Y /\ dom (f1-f2); then A7: c in X /\ Y & c in dom (f1-f2) by XBOOLE_0:def 3; then c in X & c in Y & c in (dom f1 /\ dom f2) by Def2,XBOOLE_0:def 3; then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A8: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3; thus (f1-f2)/.c = (f1/.c) - (f2/.c) by A7,Def2 .= r1 - (f2/.c) by A2,A8 .= r1 - r2 by A3,A8; end; hence (f1 - f2) is_constant_on (X /\ Y) by PARTFUN2:def 3; end; theorem for f1 be PartFunc of C,REAL holds f1 is_constant_on X & f2 is_constant_on Y implies (f1 (#) f2) is_constant_on (X /\ Y) proof let f1 be PartFunc of C,REAL; assume A1: f1 is_constant_on X & f2 is_constant_on Y; then consider r1 such that A2: for c st c in X /\ dom f1 holds f1.c = r1 by PARTFUN2:76; consider r2 being VECTOR of V such that A3: for c st c in Y /\ dom f2 holds (f2/.c) = r2 by A1,PARTFUN2:def 3; now let c; assume c in X /\ Y /\ dom (f1(#)f2); then A4: c in X /\ Y & c in dom (f1(#)f2) by XBOOLE_0:def 3; then A5: c in X & c in Y & c in (dom f1 /\ dom f2) by Def3,XBOOLE_0:def 3; then c in dom f1 & c in dom f2 by XBOOLE_0:def 3; then A6: c in X /\ dom f1 & c in Y /\ dom f2 by A5,XBOOLE_0:def 3; thus (f1(#)f2)/.c = f1.c * (f2/.c) by A4,Def3 .= r1 * (f2/.c) by A2,A6 .= r1 * r2 by A3,A6; end; hence thesis by PARTFUN2:def 3; end; theorem Th59: f is_constant_on Y implies p(#)f is_constant_on Y proof assume f is_constant_on Y; then consider r being VECTOR of V such that A1: for c st c in Y /\ dom f holds f/.c = r by PARTFUN2:def 3; now let c; assume c in Y /\ dom (p(#)f); then A2: c in dom (p(#)f) & c in Y by XBOOLE_0:def 3; then c in dom f by Def4; then A3: c in Y /\ dom f by A2,XBOOLE_0:def 3; thus (p(#)f)/.c = p * f/.c by A2,Def4 .= p*r by A1,A3; end; hence thesis by PARTFUN2:def 3; end; theorem Th60: f is_constant_on Y implies ||.f.|| is_constant_on Y & -f is_constant_on Y proof assume f is_constant_on Y; then consider r being VECTOR of V such that A1: for c st c in Y /\ dom f holds f/.c = r by PARTFUN2:def 3; now let c; assume c in Y /\ dom (||.f.||); then A2: c in dom (||.f.||) & c in Y by XBOOLE_0:def 3; then c in dom f by Def5; then A3: c in Y /\ dom f by A2,XBOOLE_0:def 3; thus (||.f.||).c = ||.f/.c.|| by A2,Def5 .= ||.r.|| by A1,A3; end; hence ||.f.|| is_constant_on Y by PARTFUN2:76; now take p=-r; let c; assume A4: c in Y /\ dom (-f); then c in Y /\ dom f by Def6; then A5: -f/.c = p by A1; c in dom (-f) by A4,XBOOLE_0:def 3; hence (-f)/.c = p by A5,Def6; end; hence thesis by PARTFUN2:def 3; end; theorem Th61: f is_constant_on Y implies f is_bounded_on Y proof assume f is_constant_on Y; then consider r being VECTOR of V such that A1: for c st c in Y /\ dom f holds f/.c = r by PARTFUN2:def 3; now take p=||.r.||; let c; assume c in Y /\ dom f; hence ||.f/.c.|| <= p by A1; end; hence thesis by Def7; end; theorem f is_constant_on Y implies (for r holds r(#)f is_bounded_on Y) & (-f is_bounded_on Y) & ||.f.|| is_bounded_on Y proof assume A1: f is_constant_on Y; now let r; r(#)f is_constant_on Y by A1,Th59; hence r(#)f is_bounded_on Y by Th61; end; hence for r holds r(#)f is_bounded_on Y; -f is_constant_on Y by A1,Th60; hence -f is_bounded_on Y by Th61; ||.f.|| is_constant_on Y by A1,Th60 ; hence ||.f.|| is_bounded_on Y by RFUNCT_1:108; end; theorem f1 is_bounded_on X & f2 is_constant_on Y implies f1+f2 is_bounded_on (X /\ Y) proof assume A1: f1 is_bounded_on X & f2 is_constant_on Y; then f2 is_bounded_on Y by Th61; hence thesis by A1,Th53; end; theorem f1 is_bounded_on X & f2 is_constant_on Y implies f1-f2 is_bounded_on X /\ Y & f2-f1 is_bounded_on X /\ Y proof assume A1: f1 is_bounded_on X & f2 is_constant_on Y; then A2: f2 is_bounded_on Y by Th61; then -f1 is_bounded_on X & -f2 is_bounded_on Y by A1,Th52; then f1+-f2 is_bounded_on X /\ Y & f2+-f1 is_bounded_on Y /\ X by A1,A2,Th53 ; hence thesis by Th31; end;

Back to top