Copyright (c) 1992 Association of Mizar Users
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;