let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let V be ComplexNormSpace; :: thesis: for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let f2 be PartFunc of M,V; :: thesis: for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let X, Y be set ; :: thesis: for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
let f1 be PartFunc of M,COMPLEX; :: thesis: ( f1 | X is constant & f2 | Y is constant implies (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
consider z1 being Element of COMPLEX such that
A3: for c being Element of M st c in X /\ (dom f1) holds
f1 . c = z1 by A1, PARTFUN2:57;
consider r2 being VECTOR of V such that
A4: for c being Element of M st c in Y /\ (dom f2) holds
f2 /. c = r2 by A2, PARTFUN2:35;
now :: thesis: for c being Element of M st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
(f1 (#) f2) /. c = z1 * r2
let c be Element of M; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = z1 * r2 )
assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: (f1 (#) f2) /. c = z1 * r2
then A6: c in X /\ Y by XBOOLE_0:def 4;
then A7: c in Y 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 Def1;
then A10: c in dom f1 by XBOOLE_0:def 4;
then A11: f1 /. c = f1 . c by PARTFUN1:def 6;
c in dom f2 by A9, XBOOLE_0:def 4;
then A12: c in Y /\ (dom f2) by A7, XBOOLE_0:def 4;
c in X by A6, XBOOLE_0:def 4;
then A13: c in X /\ (dom f1) by A10, XBOOLE_0:def 4;
thus (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by A8, Def1
.= z1 * (f2 /. c) by A3, A13, A11
.= z1 * r2 by A4, A12 ; :: thesis: verum
end;
hence (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:35; :: thesis: verum