let X, Y be set ; :: thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX 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,COMPLEX 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,COMPLEX; :: 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 cr1 being Element of COMPLEX such that
A3: for c being Element of C st c in X /\ (dom f1) holds
f1 /. c = cr1 by A1, PARTFUN2:35;
consider cr2 being Element of COMPLEX such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = cr2 by A2, PARTFUN2:35;
A5: cr1 + cr2 in COMPLEX by XCMPLX_0:def 2;
now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
(f1 + f2) /. c = cr1 + cr2
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = cr1 + cr2 )
assume A6: c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: (f1 + f2) /. c = cr1 + cr2
then A7: c in X /\ Y by XBOOLE_0:def 4;
then A8: c in X by XBOOLE_0:def 4;
A9: c in dom (f1 + f2) by A6, XBOOLE_0:def 4;
then A10: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then A11: c in X /\ (dom f1) by A8, XBOOLE_0:def 4;
A12: c in Y by A7, XBOOLE_0:def 4;
c in dom f2 by A10, XBOOLE_0:def 4;
then A13: c in Y /\ (dom f2) by A12, XBOOLE_0:def 4;
thus (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by A9, Th1
.= cr1 + (f2 /. c) by A3, A11
.= cr1 + cr2 by A4, A13 ; :: thesis: verum
end;
hence (f1 + f2) | (X /\ Y) is constant by A5, PARTFUN2:35; :: thesis: ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
A14: cr1 - cr2 in COMPLEX by XCMPLX_0:def 2;
now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 - f2)) holds
(f1 - f2) /. c = cr1 - cr2
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = cr1 - cr2 )
assume A15: c in (X /\ Y) /\ (dom (f1 - f2)) ; :: thesis: (f1 - f2) /. c = cr1 - cr2
then A16: c in X /\ Y by XBOOLE_0:def 4;
then A17: c in X by XBOOLE_0:def 4;
A18: c in dom (f1 - f2) by A15, XBOOLE_0:def 4;
then A19: c in (dom f1) /\ (dom f2) by Th2;
then c in dom f1 by XBOOLE_0:def 4;
then A20: c in X /\ (dom f1) by A17, XBOOLE_0:def 4;
A21: c in Y by A16, XBOOLE_0:def 4;
c in dom f2 by A19, XBOOLE_0:def 4;
then A22: c in Y /\ (dom f2) by A21, XBOOLE_0:def 4;
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A18, Th2
.= cr1 - (f2 /. c) by A3, A20
.= cr1 - cr2 by A4, A22 ; :: thesis: verum
end;
hence (f1 - f2) | (X /\ Y) is constant by A14, PARTFUN2:35; :: thesis: (f1 (#) f2) | (X /\ Y) is constant
A23: cr1 * cr2 in COMPLEX by XCMPLX_0:def 2;
now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
(f1 (#) f2) /. c = cr1 * cr2
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = cr1 * cr2 )
assume A24: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: (f1 (#) f2) /. c = cr1 * cr2
then A25: c in X /\ Y by XBOOLE_0:def 4;
then A26: c in X by XBOOLE_0:def 4;
A27: c in dom (f1 (#) f2) by A24, XBOOLE_0:def 4;
then A28: c in (dom f1) /\ (dom f2) by Th3;
then c in dom f1 by XBOOLE_0:def 4;
then A29: c in X /\ (dom f1) by A26, XBOOLE_0:def 4;
A30: c in Y by A25, XBOOLE_0:def 4;
c in dom f2 by A28, XBOOLE_0:def 4;
then A31: c in Y /\ (dom f2) by A30, XBOOLE_0:def 4;
thus (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by A27, Th3
.= cr1 * (f2 /. c) by A3, A29
.= cr1 * cr2 by A4, A31 ; :: thesis: verum
end;
hence (f1 (#) f2) | (X /\ Y) is constant by A23, PARTFUN2:35; :: thesis: verum