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 A1: ( f1 | X is constant & f2 | Y is constant ) ; :: thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
then consider cr1 being Element of COMPLEX such that
A2: for c being Element of C st c in X /\ (dom f1) holds
f1 /. c = cr1 by PARTFUN2:54;
consider cr2 being Element of COMPLEX such that
A3: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = cr2 by A1, PARTFUN2:54;

now

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = cr1 + cr2 )
assume c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: (f1 + f2) /. c = cr1 + cr2
then A4: ( c in X /\ Y & c in dom (f1 + f2) ) by XBOOLE_0:def 4;
then ( c in X & c in Y & c in (dom f1) /\ (dom f2) ) by VALUED_1:def 1, XBOOLE_0:def 4;
then ( c in X & c in Y & c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A5: ( c in X /\ (dom f1) & c in Y /\ (dom f2) ) by XBOOLE_0:def 4;
thus (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by A4, Th3
.= cr1 + (f2 /. c) by A2, A5
.= cr1 + cr2 by A3, A5 ; :: thesis: verum

end;

hence (f1 + f2) | (X /\ Y) is constant by PARTFUN2:54; :: thesis: ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )

now

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = cr1 - cr2 )
assume c in (X /\ Y) /\ (dom (f1 - f2)) ; :: thesis: (f1 - f2) /. c = cr1 - cr2
then A6: ( c in X /\ Y & c in dom (f1 - f2) ) by XBOOLE_0:def 4;
then ( c in X & c in Y & c in (dom f1) /\ (dom f2) ) by Th4, XBOOLE_0:def 4;
then ( c in X & c in Y & c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A7: ( c in X /\ (dom f1) & c in Y /\ (dom f2) ) by XBOOLE_0:def 4;
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A6, Th4
.= cr1 - (f2 /. c) by A2, A7
.= cr1 - cr2 by A3, A7 ; :: thesis: verum

end;

hence (f1 - f2) | (X /\ Y) is constant by PARTFUN2:54; :: thesis: (f1 (#) f2) | (X /\ Y) is constant

now

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = cr1 * cr2 )
assume c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: (f1 (#) f2) /. c = cr1 * cr2
then A8: ( c in X /\ Y & c in dom (f1 (#) f2) ) by XBOOLE_0:def 4;
then ( c in X & c in Y & c in (dom f1) /\ (dom f2) ) by Th5, XBOOLE_0:def 4;
then ( c in X & c in Y & c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A9: ( c in X /\ (dom f1) & c in Y /\ (dom f2) ) by XBOOLE_0:def 4;
thus (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by A8, Th5
.= cr1 * (f2 /. c) by A2, A9
.= cr1 * cr2 by A3, A9 ; :: thesis: verum

end;

hence (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:54; :: thesis: verum