let X, Y be set ; :: thesis: for C being non empty set

for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds

( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds

( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

let f1, f2 be PartFunc of C,REAL; :: thesis: ( f1 | X is constant & f2 | Y is constant implies ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) )

assume that

A1: f1 | X is constant and

A2: f2 | Y is constant ; :: thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

consider r1 being Element of REAL such that

A3: for c being Element of C st c in X /\ (dom f1) holds

f1 . c = r1 by A1, PARTFUN2:57;

consider r2 being Element of REAL such that

A4: for c being Element of C st c in Y /\ (dom f2) holds

f2 . c = r2 by A2, PARTFUN2:57;

for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds

( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds

( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

let f1, f2 be PartFunc of C,REAL; :: thesis: ( f1 | X is constant & f2 | Y is constant implies ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) )

assume that

A1: f1 | X is constant and

A2: f2 | Y is constant ; :: thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

consider r1 being Element of REAL such that

A3: for c being Element of C st c in X /\ (dom f1) holds

f1 . c = r1 by A1, PARTFUN2:57;

consider r2 being Element of REAL such that

A4: for c being Element of C st c in Y /\ (dom f2) holds

f2 . c = r2 by A2, PARTFUN2:57;

now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds

(f1 + f2) . c = r1 + r2

hence
(f1 + f2) | (X /\ Y) is constant
by PARTFUN2:57; :: thesis: ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )(f1 + f2) . c = r1 + r2

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) . c = r1 + r2 )

assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: (f1 + f2) . c = r1 + r2

then A6: c in X /\ Y by XBOOLE_0:def 4;

then A7: c in X by XBOOLE_0:def 4;

A8: c in dom (f1 + f2) by A5, XBOOLE_0:def 4;

then A9: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;

then c in dom f1 by XBOOLE_0:def 4;

then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def 4;

A11: c in Y by A6, XBOOLE_0:def 4;

c in dom f2 by A9, XBOOLE_0:def 4;

then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def 4;

thus (f1 + f2) . c = (f1 . c) + (f2 . c) by A8, VALUED_1:def 1

.= r1 + (f2 . c) by A3, A10

.= r1 + r2 by A4, A12 ; :: thesis: verum

end;assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: (f1 + f2) . c = r1 + r2

then A6: c in X /\ Y by XBOOLE_0:def 4;

then A7: c in X by XBOOLE_0:def 4;

A8: c in dom (f1 + f2) by A5, XBOOLE_0:def 4;

then A9: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;

then c in dom f1 by XBOOLE_0:def 4;

then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def 4;

A11: c in Y by A6, XBOOLE_0:def 4;

c in dom f2 by A9, XBOOLE_0:def 4;

then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def 4;

thus (f1 + f2) . c = (f1 . c) + (f2 . c) by A8, VALUED_1:def 1

.= r1 + (f2 . c) by A3, A10

.= r1 + r2 by A4, A12 ; :: thesis: verum

now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 - f2)) holds

(f1 - f2) . c = r1 - r2

hence
(f1 - f2) | (X /\ Y) is constant
by PARTFUN2:57; :: thesis: (f1 (#) f2) | (X /\ Y) is constant (f1 - f2) . c = r1 - r2

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) . c = r1 - r2 )

assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; :: thesis: (f1 - f2) . c = r1 - r2

then A14: c in X /\ Y by XBOOLE_0:def 4;

then A15: c in X by XBOOLE_0:def 4;

A16: c in dom (f1 - f2) by A13, XBOOLE_0:def 4;

then A17: c in (dom f1) /\ (dom f2) by VALUED_1:12;

then c in dom f1 by XBOOLE_0:def 4;

then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def 4;

A19: c in Y by A14, XBOOLE_0:def 4;

c in dom f2 by A17, XBOOLE_0:def 4;

then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def 4;

thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A16, VALUED_1:13

.= r1 - (f2 . c) by A3, A18

.= r1 - r2 by A4, A20 ; :: thesis: verum

end;assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; :: thesis: (f1 - f2) . c = r1 - r2

then A14: c in X /\ Y by XBOOLE_0:def 4;

then A15: c in X by XBOOLE_0:def 4;

A16: c in dom (f1 - f2) by A13, XBOOLE_0:def 4;

then A17: c in (dom f1) /\ (dom f2) by VALUED_1:12;

then c in dom f1 by XBOOLE_0:def 4;

then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def 4;

A19: c in Y by A14, XBOOLE_0:def 4;

c in dom f2 by A17, XBOOLE_0:def 4;

then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def 4;

thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A16, VALUED_1:13

.= r1 - (f2 . c) by A3, A18

.= r1 - r2 by A4, A20 ; :: thesis: verum

now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds

(f1 (#) f2) . c = r1 * r2

hence
(f1 (#) f2) | (X /\ Y) is constant
by PARTFUN2:57; :: thesis: verum(f1 (#) f2) . c = r1 * r2

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) . c = r1 * r2 )

assume A21: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: (f1 (#) f2) . c = r1 * r2

then A22: c in X /\ Y by XBOOLE_0:def 4;

c in dom (f1 (#) f2) by A21, XBOOLE_0:def 4;

then A23: c in (dom f1) /\ (dom f2) by VALUED_1:def 4;

then A24: c in dom f1 by XBOOLE_0:def 4;

A25: c in dom f2 by A23, XBOOLE_0:def 4;

c in Y by A22, XBOOLE_0:def 4;

then A26: c in Y /\ (dom f2) by A25, XBOOLE_0:def 4;

c in X by A22, XBOOLE_0:def 4;

then A27: c in X /\ (dom f1) by A24, XBOOLE_0:def 4;

thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by VALUED_1:5

.= r1 * (f2 . c) by A3, A27

.= r1 * r2 by A4, A26 ; :: thesis: verum

end;assume A21: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: (f1 (#) f2) . c = r1 * r2

then A22: c in X /\ Y by XBOOLE_0:def 4;

c in dom (f1 (#) f2) by A21, XBOOLE_0:def 4;

then A23: c in (dom f1) /\ (dom f2) by VALUED_1:def 4;

then A24: c in dom f1 by XBOOLE_0:def 4;

A25: c in dom f2 by A23, XBOOLE_0:def 4;

c in Y by A22, XBOOLE_0:def 4;

then A26: c in Y /\ (dom f2) by A25, XBOOLE_0:def 4;

c in X by A22, XBOOLE_0:def 4;

then A27: c in X /\ (dom f1) by A24, XBOOLE_0:def 4;

thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by VALUED_1:5

.= r1 * (f2 . c) by A3, A27

.= r1 * r2 by A4, A26 ; :: thesis: verum