let X, Y be set ; 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 ; 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; ( 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
; ( (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;
hence
(f1 + f2) | (X /\ Y) is constant
by A5, PARTFUN2:35; ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
A14:
cr1 - cr2 in COMPLEX
by XCMPLX_0:def 2;
hence
(f1 - f2) | (X /\ Y) is constant
by A14, PARTFUN2:35; (f1 (#) f2) | (X /\ Y) is constant
A23:
cr1 * cr2 in COMPLEX
by XCMPLX_0:def 2;
hence
(f1 (#) f2) | (X /\ Y) is constant
by A23, PARTFUN2:35; verum